src/ZF/Tools/datatype_package.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-26 wenzelm 2011-04-26 structure Cla as defined in FOL;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-16 wenzelm 2010-05-16 prefer structure Parse_Spec;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-27 wenzelm 2010-03-27 moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2010-02-19 wenzelm 2010-02-19 moved ancient Drule.get_def to OldGoals.get_def;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
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;