Renamed letI to LetI (for consistency)

Added discussion of "let" and pattern-matching

Stylistic changes to discussion of pattern-matching

Added a verified verification-condition generator.

Ran expandshort

Now expands TABS as well

trivial updates

New version number

*** empty log message ***

added Lattice demo;

added this stuff;

improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);

added comments

beautified file_info a bit

fixed bug in file_info

Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.

simplified file_info by using System.filedate

removed reference to Nat thms in elim_rls.

Minor mod.

Polished proofs.

Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule.

Modified non-empty-types warning in HOL.

Reduced indentation; no change in function

Purely cosmetic changes

Updated comments for compression functions

Removed unfold:thm from signature INTR_ELIM and from the functor result. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store.

Now mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.

fixed indentation