src/ZF/Tools/datatype_package.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
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-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-18 wenzelm 2008-11-18 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;
2008-10-23 wenzelm 2008-10-23 Thm.get_def;
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-18 wenzelm 2008-06-18 eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-01 wenzelm 2008-03-01 tuned ML code, more antiquotations;
2008-03-01 wenzelm 2008-03-01 misc cleanup of embedded ML code; use more antiquotations; tuned;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2008-01-26 wenzelm 2008-01-26 avoid redundant escaping of Isabelle symbols;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-09-26 wenzelm 2007-09-26 Attrib.eval_thms;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.mk_defpair;
2007-06-19 wenzelm 2007-06-19 BalancedTree;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-15 wenzelm 2006-01-15 classical attributes: optional weight;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
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-11-16 wenzelm 2005-11-16 Term.betapplys;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 wenzelm 2005-10-19 removed obsolete add_datatype_x; tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
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.
2005-01-24 berghofe 2005-01-24 Replaced xstring by thmref.
2002-05-15 paulson 2002-05-15 better error messages for datatypes not declared Const
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-11-19 wenzelm 2001-11-19 tuned;
2001-11-16 wenzelm 2001-11-16 additional P.marg_comment;
2001-11-14 wenzelm 2001-11-14 use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-09 wenzelm 2001-11-09 adapted to add_inductive_x;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-05-05 wenzelm 2000-05-05 use Sign.simple_read_term;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-01-13 paulson 2000-01-13 change in add_thmss to suppress warning
1999-10-04 wenzelm 1999-10-04 tuned;