src/HOL/Tools/typedef_package.ML
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-10 wenzelm 2006-01-10 generic attributes;
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-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-19 wenzelm 2005-10-19 removed obsolete add_typedef_x; tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 tuned Isar interfaces; tuned IsarThy.theorem_i;
2005-09-06 wenzelm 2005-09-06 proper treatment of polymorphic sets; tuned;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-25 berghofe 2005-08-25 Implemented incremental code generation.
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-07-01 berghofe 2005-07-01 Adapted to modular code generation.
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-05-31 wenzelm 2005-05-31 fixed outer syntax: allow type_args with parentheses;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-10-27 berghofe 2004-10-27 Added type constraint to make SML/NJ happy.
2004-10-26 berghofe 2004-10-26 Added simple code generator.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 Library.read_int;
2004-04-15 wenzelm 2004-04-15 finalconsts RepC AbsC;
2002-08-02 wenzelm 2002-08-02 typedef: "open" option;
2002-07-24 wenzelm 2002-07-24 adapted fact names;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-10 wenzelm 2002-01-10 simplified IsarThy.theorem_i;
2002-01-03 wenzelm 2002-01-03 tuned msg;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-04 wenzelm 2001-11-04 IsarThy.theorem_i (None, []);
2001-10-31 wenzelm 2001-10-31 IsarThy.theorem_i: no locale;
2001-10-27 wenzelm 2001-10-27 use Tactic.prove;
2001-10-18 wenzelm 2001-10-18 sane internal interface for add_typedef(_i);
2001-10-17 wenzelm 2001-10-17 improved internal interface of typedef;
2001-10-16 wenzelm 2001-10-16 typedef: export result;
2001-10-13 wenzelm 2001-10-13 'morphisms' spec; tuned goal pattern for set;
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-10-12 wenzelm 2001-10-12 test: use SkipProof.make_thm instead of Thm.assume;
2001-09-27 wenzelm 2001-09-27 renamed theory "subset" to "Typedef";
2001-07-15 wenzelm 2001-07-15 abtract non-emptiness statements (no longer use Eps); cleaned up;
2000-12-19 wenzelm 2000-12-19 improved errors;
2000-12-14 wenzelm 2000-12-14 'typedef': present result theorem "type_definition Rep Abs A";
2000-12-06 wenzelm 2000-12-06 less rude treatment of "no_def";
2000-11-13 wenzelm 2000-11-13 tuned IsarThy.theorem_i;
2000-10-19 wenzelm 2000-10-19 provide more theorems (see subset.thy); tuned;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-07-01 wenzelm 2000-07-01 GPLed;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-01-25 wenzelm 2000-01-25 fallback on PureThy version;
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-09-04 wenzelm 1999-09-04 goal_nonempty: Ex goal for new-style version;
1999-08-02 wenzelm 1999-08-02 tuned outer syntax;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;