src/HOL/Tools/datatype_rep_proofs.ML
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
2009-01-07 wenzelm 2009-01-07 inductive: added fork_mono flag;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-22 haftmann 2008-10-22 tuned typedef interface
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-09-25 wenzelm 2008-09-25 explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove; tuned list operations;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-20 haftmann 2008-06-20 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
2008-05-28 haftmann 2008-05-28 moved distinctness_limit to datatype_rep_proofs.ML
2008-05-23 haftmann 2008-05-23 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-03 berghofe 2008-04-03 - use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package
2008-03-29 wenzelm 2008-03-29 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
2008-03-20 haftmann 2008-03-20 more antiquotations
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-25 wenzelm 2008-02-25 inductive package: simplified group handling;
2008-01-26 wenzelm 2008-01-26 internal inductive: fresh theorem group;
2007-12-17 berghofe 2007-12-17 Adapted to changes in interface of indtac.
2007-10-02 wenzelm 2007-10-02 inductive: mark internal theorems as Thm.internalK;
2007-09-28 berghofe 2007-09-28 Adapted to changes in interface of add_inductive_i.
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-08-01 wenzelm 2007-08-01 simplified internal Config interface;
2007-07-31 wenzelm 2007-07-31 replaced dtK ref by datatype_distinctness_limit configuration option;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-06-19 wenzelm 2007-06-19 BalancedTree;
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-11-26 wenzelm 2006-11-26 InductivePackage.add_inductive_global;
2006-11-14 wenzelm 2006-11-14 InductivePackage.add_inductive_i: canonical argument order;
2006-11-10 wenzelm 2006-11-10 simplified LocalTheory.exit;
2006-10-13 berghofe 2006-10-13 Adapted to new inductive definition package.
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-05-02 wenzelm 2006-05-02 ThyInfo.the_theory;
2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-02 haftmann 2005-12-02 introduced new map2, fold
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
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.