src/ZF/Tools/inductive_package.ML
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-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29 wenzelm 2010-04-29 more explicit treatment of context, although not fully localized;
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-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
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-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-19 wenzelm 2009-03-19 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
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-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
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-02 wenzelm 2009-01-02 MetaSimplifier.SIMPLIFIER;
2009-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
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-25 wenzelm 2008-06-25 tuned;
2008-06-18 wenzelm 2008-06-18 eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-17 wenzelm 2008-04-17 adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-15 wenzelm 2008-03-15 proper 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-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-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-09-26 wenzelm 2007-09-26 Attrib.eval_thms; Syntax.parse/check;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-08-14 wenzelm 2007-08-14 PrimitiveDefs.mk_defpair;
2007-06-19 wenzelm 2007-06-19 BalancedTree;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;