README for Twelf 1.2R8

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.
 - Constraint solving modules for:
     rationals
     integers
     strings
     booleans
 - Hierarchical configuration files