added nested types on right hand side of datatype definitions

removed list2 and enum2

added enum2 and list2

Removed duplicate copy of converse_Un

Various axiomatic type class demos;

the NatClass demo of the axclass tutorial;

fixed bug: duplicate "duplicate" warnings

restored old invocation of use_string till I can make the new version work

added global simpset

added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database

added same_sg and same_thm

adapted to new version of shyps-stuff;

nonempty_sort: no longer var names as args;

considerably tuned shyps handling;

adapted to new version of shyps-stuff;

added check for duplicate theorems in theorem database; changed warnings and error messages in thy_read to distinguish between theorems in theor_y_ database and in theor_em_ database

minor fix to make less noise with SML/NJ;

updated "o" in HOL: (infixl 55) added warning about conj_cong in HOL.

minor corrections to indexing; added thms_containing in header

changed "o" to (infixl 55)

clarified comment

fixed bug in findI removed duplicates in findEs

deactivated fix_shyps.

updated version number to revision 4

Mateja Jamnik's theory to html converter

Handle renaming of CHOL.tex to HOL.tex

minor polishing of text on findI, etc.

Trivial reformatting of reference

corrected bind_thm: now applies "standard" uniformly.

Documented findI, findE, findEs, thms_containing.

Added findI, findEs, and findE.

MAJOR changes: added shyps component to type thm; added rules strip_shyps, implies_intr_shyps; fixed rules to handle shyps properly;

modified prepare_proof to handle shyps;

modified pretty_thm, standard, eq_thm to handle shyps;

modified prep_thm_axm to handle shyps; fixed class_axms: class_trivs *first*; improved axclass_tac: now also handles object rules as witnesses;

added (my own version of) nonempty_sort: sg -> (string * sort) list -> sort -> bool;

added nonempty_sort (a somewhat braindead version!);

Added nonempty_sort.

added section on "Reordering assumptions".

added rotate_tac

changed AC_... to OrdQuant_...

Version of the proof macros for LaTeX 2.09

added rotate_tac.

Ran expandshort and corrected spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Ran expandshort and changed spelling of Grabczewski

Added rev_append and rev_rev_ident to list_ss.

minor fix: instance now raises error if witness axioms don't exist;

Many small changes to make proofs run faster

Now includes all the AC files

tidied proof of add_less_mono

trivial updates to header and bibliography

Numerous small improvements by KG and LCP

match_bvs no longer puts a name in the alist if it is null ("")

Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)

Corrected mixfix declaration of @perm

Proved perm_length

Added two final lines to intro_tacsf for mutual recursion (borrowed from ZF version)

Old version of mutual induction never worked. Now ensures that all predicates get the SAME type. Updated mutual_ind_tac from ZF version

Changed comments

Added Part_Int and Part_Collect for inductive definitions