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 formbshow [ tree | grind ]
shows abstracted Bool termbresolve [ <num1> [ { <num2> | all } ] ]
shows assignments which make abstracted Bool term truebguess { 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 formeq lhs = true
a premise of a goal sentence - new tactic
rd-
which is similar tord
but cancels the normalization of the goal sentence if the sentence is not satisfied
- new switch
tree horizontal
. if onshow 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.