CafeOBJ 1.5.5 released

We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes:

• Enhancemets of a family of Bool term inspector commands:
  • binspect [ in : <Modexpr> ] <bool-term> . converts given <bool-term> into abstracted xor-and normal form
  • bshow [ tree | grind ] shows abstracted Bool term
  • bresolve [ <num1> [ { <num2> | all } ] ] shows assignments which make abstracted Bool term true
  • bguess { imply | and | or } tries with some heuristics to solve the abstracted Bool term
• bug fix in ACZ rewriting
• CITP changes
  • :ctf [ <term> ] accepts constructors with arguments
  • new command :imply to make instantiated lhs of existing equation of the form eq lhs = true a premise of a goal sentence
  • new tactic rd- which is similar to rd but cancels the normalization of the goal sentence if the sentence is not satisfied
• new switch tree horizontal. if on show term tree displays the term tree structure horizontally (default off).

Please see the download page for the source release, binary packages, and installation instructions.

CafeOBJ 1.5.5 has already been uploaded to Debian, see http://packages.debian.org/cafeobj. The MacPort is also updated.

Please report bugs to our bug tracker.