* CafeOBJ 1.6.0
===============
- CITP is officially renamed to PTCalc
. but documents are not updated yet
- PTCalc(CITP) enhacements
. :init defined by :def is evaluated in the proof node to which it is applied
. :init without substitution can be
- Search predicate enhancements
. nested search is properly handled
. 'show path' accepts state specifier of the form 'depth-state'
- Several bug fixes
* CafeOBJ 1.5.8
===============
- Several bug fixes
. make 'variables as constants' to only apply in the context of :init
. id-completion should not aplied to non-exec axioms
. minor bug fixes in making id conditions
. fix inapropreate context handling in parameterized module
- New command :bgrind/bgrind
. prints xor-and normal form in 'grind' manner
* CafeOBJ 1.5.7
===============
- CITP enhancements
- adaption for newer SBCL
* CafeOBJ 1.5.6
===============
- CITP enhancements
* CafeOBJ 1.5.5
===============
- 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).
* CafeOBJ 1.5.4
===============
- CITP changes
. new commands :ctf- and :csp-
. new command :def(ine) to turn :ctf(-) and :csp(-) into proper
tactics for :apply
. new tactics nf, ct
- improvements in the online help system
- bug fixes in AC rewriting
- small changes in the set of abbreviations of the Emacs mode
- module system: require/provide can use Perl style :: separators
to load modules from the libpath and its sub-directories
- term inspection (binspect) to analyze xor terms
* CafeOBJ 1.5.3
===============
- interpreter functions
. 'describe module tree' (new) - prints out module importing structure
. multi-line comments delimited by #| and |#
. 'show modules' - does not print out hidden modules
. 'preds' (new) - declare multiple Bool ops at once
. new abbreviations: tr, ctr, pd, pds, bpd, bpds (for trans, ctrans,
pred, preds, bpred, bpreds, respectively)
. new meta label: :m-and-also, :m-or-else
- CITP changes
. new command :ctf, :csp
. modules generated in CITP are hidden
* CafeOBJ 1.5.2
===============
- Fixes to the wrapper to work with spaces in the path
- make 'ls' command work on Windows (but not UNC path)
* CafeOBJ 1.5.1
===============
Fixes for Windows packages to be run from UNC paths
* CafeOBJ 1.5.0
===============
Several changes have been done over years, we summarize only a few:
- introduction of a large family of search predicates for state/transition
based specifications (see `search predicates' in the online help or
manual)
- addition of a (nearly) complete reference manual (reference-manual.pdf)
- addition of CITP-like proving tool
(see http://www.jaist.ac.jp/~danielmg/citp.html for the original version)
- revised build system, allows for building and running CafeOBJ based
on several lisp engines
- improved online help system with search functionality (see `?' `?ap' etc)
- build support has been stream-lined, currently supported Common Lisp
implementations are SBCL, CLISP, Allegro CL
- ...
* many unmentioned releases
* CafeOBJ 1.4.3PigNose
=======================
a resolution based proof eningine PigNose.
* Changes in CafeOBJ 1.4.3
===========================
various minor bug fixes
* Changes in CafeOBJ 1.4.2b10
=============================
** new `check' command
check { coherency | coherence | coh } [ <OpName> ]
checks if operator is behaviouraly coherent
* Changes in CafeOBJ 1.4.2b9
============================
** switch `fast parse' is obsolete
* Changes in CafeOBJ 1.4.2b4
============================
** switch `mel always' now properly works for `parse' command.
** supports qulifying operator symbols by module name in terms.
** faster version of term parser for ad-hoc overloading operators.
relating top-level switch: `fast parse', default on.
** made nesting limit of evaluating condition part. this prevents
unexpected break in underlying Lisp system for many of the cases.
related switch: `cond limit', accepting `.'(no limit) and positive
integer. defaults value varies among underlying lisp.
* Changes in CafeOBJ 1.4.2b2
============================
** Specifying views to parameters are easier for modules like:
mod FOO (X :: TH1, Y :: TH2(X)) { ... }
* Changes in CafeOBJ 1.4.2b1
============================
This version has some experimental new features and several bug
fixes.
** In addition to Gnu Common Lisp, CMU Common Lisp and Allegro Common Lisp
can be used as a platform (see README and INSTALL for detail).
** Faster rewrite engine `brute' is now available, and can be invoked from
CafeOBJ.
** Behavioural axioms can be used in equational reduction, and an operator
attribute `coherent' is added for this purpose.
** A behavioural reduction command is introduced.
** Sort predicates (a partial MEL support) are introduced (experimental).
Unfortunately, full implementation of `record' construct is not yet
finished in this version.
$Id: CHANGES,v 1.1.1.1 2003-06-19 08:25:55 sawada Exp $