NEWS

* CafeOBJ 1.6.0
===============

  - CITP is officially renamed to PTCalc
    . but documents are not updated yet
  - PTCalc(CITP) enhancements
    . :init defined by :def is evaluated in the proof node to which it is applied
    . :init can be without substitution
  - 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 $