src/HOL/Tools/datatype_realizer.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 Thm.proof_of returns proof_body;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2008-03-20 haftmann 2008-03-20 more antiquotations
2007-10-29 wenzelm 2007-10-29 qualified Proofterm.proofs;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 simplified interpretation setup;
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.frees/vars_of etc.;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
2005-05-31 wenzelm 2005-05-31 Theory.restore_naming;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-10-26 berghofe 2004-10-26 Fixed problem with sorts in function make_casedists.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-11-27 berghofe 2002-11-27 Changed format of realizers / correctness proofs.
2002-11-13 berghofe 2002-11-13 prove_goal' -> Goal.simple_prove_goal_cterm
2002-10-21 berghofe 2002-10-21 Changed type of Logic.strip_horn.
2002-10-10 berghofe 2002-10-10 Reimplemented parts of datatype package dealing with datatypes involving function types. Now also supports functions with more than one argument.
2002-08-07 berghofe 2002-08-07 Module for defining realizers for induction and case analysis theorems for datatypes.