src/HOL/Tools/typedef_package.ML
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2007-12-05 haftmann 2007-12-05 interpretation of typedefs
2007-11-30 haftmann 2007-11-30 interpretation for typedefs
2007-11-28 wenzelm 2007-11-28 ObjectLogic.typedecl;
2007-11-23 haftmann 2007-11-23 separated typedecl module, providing typedecl command with interpretation
2007-10-09 wenzelm 2007-10-09 AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned Induct interface: prefer pred'' over set'';
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.mk_defpair;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-21 wenzelm 2006-11-21 simplified Proof.theorem(_i);
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface;
2006-11-14 wenzelm 2006-11-14 removed legacy read/cert/string_of; removed obsolete IsarThy.theorem_i; tuned comments;
2006-09-06 haftmann 2006-09-06 TypedefPackage.add_typedef_* now yields name of introduced type constructor
2006-09-01 wenzelm 2006-09-01 signature: do not export private stuff;
2006-08-08 haftmann 2006-08-08 fixed code generator theorem generation
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-05-24 wenzelm 2006-05-24 simplified info/get_info; Rep/Abs: Theory.add_deps; tuned;
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-30 wenzelm 2006-04-30 AxClass.axiomatize_arity_i;
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-24 haftmann 2006-04-24 seperated typedef codegen from main code
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-04-06 haftmann 2006-04-06 added functions for definitional code generation
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;