src/ZF/List.ML
1999-01-27 paulson new typechecking solver for the simplifier
1999-01-19 paulson removal of the (thm list) argument of mk_cases
1999-01-13 paulson datatype package improvements
1999-01-07 paulson ZF: the natural numbers as a datatype
1999-01-06 paulson induct_tac and exhaust_tac
1998-12-28 paulson new inductive, datatype and primrec packages, etc.
1998-09-22 paulson tidying
1998-08-14 paulson got rid of some goal thy commands
1998-07-15 paulson More tidying and removal of "\!\!... from Goal commands
1998-07-13 paulson Huge tidy-up: removal of leading \!\!
1998-06-22 wenzelm isatool fixgoal;
1997-11-03 wenzelm isatool fixclasimp;
1997-10-10 wenzelm fixed dots;
1997-04-23 paulson Conversion to use blast_tac
1997-02-15 oheimb reflecting my recent changes of the simplifier and classical reasoner
1997-01-09 paulson Removal of needless "addIs [equality]", etc.
1997-01-08 paulson Removal of sum_cs and eq_cs
1997-01-03 paulson Implicit simpsets and clasets for FOL and ZF
1996-09-26 paulson Ran expandshort; used stac instead of ssubst
1996-08-20 paulson Addition of function set_of_list
1996-04-18 oheimb adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
1996-01-30 clasohm expanded tabs
1995-02-27 lcp Updated comment about list_subset_univ and list_into_univ.
1994-12-14 clasohm added bind_thm for theorems defined by "standard ..."
1994-12-07 clasohm added qed and qed_goal[w]
1994-08-15 lcp ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
1994-08-12 lcp installation of new inductive/datatype sections
1994-07-26 lcp Axiom of choice, cardinality results, etc.
1994-07-15 clasohm added thy_name to Datatype_Fun's parameter
1994-07-01 clasohm replaced extend_theory by new add_* functions;
less more (0) -30 tip