Preparation for Twelf 1.4

Externally visible changes:

- Tabled abstract machine 
  
  %querytabled n A.

  will try to solve A in n stages. 
  Evaluation will stop after n stages, even if 
  evaluation is not complete. If the evaluation is completed after k stages,
  and k less than n, then evaluations stops after k stages.

  global search parameters:
  * Twelf.TableIndex.strategy  : default variant checking
 
     Twelf.TableIndex.strategy := Twelf.TableIndex.Subsumption
     Twelf.TableIndex.strategy := Twelf.TableIndex.Variant

  * Twelf.TableIndex.strengthen : default true 
     apply strengthening during abstraction on term
     (strengthening on hypothesis is not yet implemented)

  * term depth : (very experimental)) 
    forces the abstract machine to suspend a goal, if the termdepth is exceeded.
    default : termdepth = NONE
    (not used in default mode)  

- mode checking can now be done post-hoc
- %mode and %covers allows mutual declarations (using paren syntax)
- %covers mdec.  (where mdec is mode declaration)
- %total tdec.   (where tdec is termination declaration)
- %worlds wdec callpats.  (where wdec is worlds declarations)

README for Twelf 1.3

Major internal update to Twelf 1.2, available as alpha release.

Externally visible changes:

- Constraints

Type reconstruction and the logic programming engine (but not yet
the theorem prover) allow various constraint domains in the style
of constraint logic programming languages.  The main ones are
equalities and inequalities over rationals and integers.

- Tracing and Breakpoints

The logic programming engine now support tracing and setting of
breakpoints for illustration and debugging purposes.

- Theorem Prover

The theorem prover now allows quantification over regular context.  The
theorem prover will also use previously proved theorems with %prove) and
ignore those with %establish, which is otherwise equivalent.  In unsafe
mode, %assert can be used to claim theorems.  However, at present no
longer generates proof terms.

- Reduction Checking

The termination checker has been extended to verify if output arguments
to a predicate are smaller than some inputs with the %reduces
declaration.

- Signature Printing

Signatures can now be printed, also in TeX format.

- Abbreviations

Added abbreviations (%abbrev) which, unlike definition, do not need to
be strict.

- Name Preferences

Name preference declarations (%name) now allow an optional second
argument for naming of parameters.

----------------------------------------------------------------------
----------------------------------------------------------------------
README for Twelf 1.2R4

Major internal update to Twelf 1.2.

Externally visible changes:
 - bug fixes (through twelf-1-2 pl5)
 - definitions need not be strict
 - %name takes optional second argument (prefered name for parameters)
 - %assert <callpats> after Twelf.unsafe := true;
   is like %prove without proving anything
 - %establish <nat> <order> <callpats> like %prove, but result
   will never be used as a lemma in future %prove
 - Twelf.Print.sgn and Twelf.Print.prog print signature
 - Twelf.Print.TeX.sgn and Twelf.Print.TeX.prog print signature in
   TeX format (see .../twelf/tex/ directory)
 - Added tracing and breakpoints/stepping in operational semantics.
   Recommended: use pull-down menus in Emacs, since documentation
   has not been written yet.
 - Theorem prover has been generalized, but is not yet stable or
   documented.  Old %theorem commands should (mostly) still work.
----------------------------------------------------------------------
Notes on 1.2 => 1.3

? Add remark about optimize
? Remark about "mixed substitution incompleteness"
? add %_unprintable_% and appropriate action to type reconstruction.

+ Add remark about "%assert" and "safe mode"
+ Add remark about "%establish" and "%prove"
+ Add Twelf.unsafe
+ Added Chapter on constraints
+ Added section of reduction checking
+ Edited section on theorem prover
+ Add Twelf.Print.sgn
+ Add Twelf.Print.prog
+ Add TeX remarks
+ Add Twelf.Print.TeX.sgn and prog
+ Add tracing.
+ %name takes optional second argument
+ Prefix argument to a few command now selects the server buffer
+ Add Twelf.make
+ Remove strictness remarks / %abbrev
+ fixity operators can now take additional arguments
+ add Twelf prover doc /afs/cs/project/twelf/www/alpha/twelf-prover.html
+ add reduction doc /afs/cs/user/bp/www/twelf/twelf-reduction.html