src/ZF/Tools/inductive_package.ML
2010-05-05 ago 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 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 ago proper context for rule_by_tactic;
2010-04-29 ago proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-29 ago more explicit treatment of context, although not fully localized;
2010-03-27 ago moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-02-28 ago more antiquotations;
2010-02-19 ago moved ancient Drule.get_def to OldGoals.get_def;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-02 ago modernized structure Primitive_Defs;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-17 ago explicitly qualify Drule.standard;
2009-09-29 ago modernized Balanced_Tree;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-20 ago Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-19 ago proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 ago more uniform handling of binding in packages;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago 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;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2009-01-02 ago MetaSimplifier.SIMPLIFIER;
2009-01-01 ago normalized some ML type/val aliases;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-11-18 ago eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-10-23 ago Thm.get_def;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-25 ago tuned;
2008-06-18 ago eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-17 ago adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-15 ago proper antiquotations;
2008-03-01 ago misc cleanup of embedded ML code;
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments
2008-01-26 ago avoid redundant escaping of Isabelle symbols;
2007-10-07 ago modernized specifications;
2007-10-06 ago simplified interfaces for outer syntax;
2007-10-05 ago tuned Induct interface: prefer pred'' over set'';
2007-10-04 ago moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-10-03 ago avoid unnamed infixes;
2007-09-26 ago Attrib.eval_thms;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-08-14 ago PrimitiveDefs.mk_defpair;
2007-06-19 ago BalancedTree;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-03 ago removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-01-19 ago moved parts of OuterParse to SpecParse;
2006-12-30 ago removed conditional combinator;
2006-11-14 ago incorporated IsarThy into IsarCmd;
2006-08-05 ago tuned;