src/HOL/Tools/datatype_realizer.ML
2006-08-02 ago removed obsolete Drule.frees/vars_of etc.;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-02-06 ago Envir.(beta_)eta_contract;
2005-12-06 ago re-oriented some result tuples in PureThy
2005-10-21 ago OldGoals;
2005-09-20 ago introduced AList module in favor of assoc etc.
2005-05-31 ago Theory.restore_naming;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-10-26 ago Fixed problem with sorts in function make_casedists.
2004-06-21 ago Merged in license change from Isabelle2004
2002-11-27 ago Changed format of realizers / correctness proofs.
2002-11-13 ago prove_goal' -> Goal.simple_prove_goal_cterm
2002-10-21 ago Changed type of Logic.strip_horn.
2002-10-10 ago Reimplemented parts of datatype package dealing with datatypes involving
2002-08-07 ago Module for defining realizers for induction and case analysis theorems