src/HOL/Tools/inductive_realizer.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-03-30 ago removed dead code; fixed typo
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 ago modernized structure Object_Logic;
2010-02-27 ago clarified @{const_name} vs. @{const_abbrev};
2010-02-25 ago more antiquotations;
2009-11-30 ago modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-17 ago eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-13 ago modernized structure Local_Theory;
2009-11-13 ago inductive: eliminated obsolete kind;
2009-11-13 ago eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-10-29 ago eliminated some old folds;
2009-10-27 ago Datatype.read_typ: standard argument order;
2009-10-25 ago name space groups are identified by serial, not serial_string;
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-15 ago replaced String.concat by implode;
2009-07-22 ago merged, resolving trivial conflict;
2009-07-21 ago dropped ancient flat_names option
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-07-10 ago dropped find_index_eq
2009-06-23 ago tuned interfaces of datatype module
2009-06-23 ago add_datatypes does not yield particular rules any longer
2009-06-23 ago add_datatype interface yields type names and less rules
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-16 ago datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-06-04 ago avoid Library.foldl_map
2009-05-18 ago introduced Thm.generatedK
2009-05-16 ago added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-26 ago simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 ago simplified attribute setup;
2009-03-11 ago explicit Binding.qualified_name -- prevents implicitly qualified bstring;
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-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2009-01-07 ago inductive: added fork_mono flag;
2008-12-31 ago eliminated OldTerm.add_term_free_names;
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-04 ago cleaned up binding module and related code
2008-11-16 ago clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 ago name_of_thm: Proofterm.fold_proof_atoms;
2008-09-23 ago Thm.proof_of;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-24 ago default replaces arbitrary
2008-06-23 ago Logic.all/mk_equals/mk_implies;
2008-06-10 ago polished interface of datatype package
2008-05-17 ago structure Display: less pervasive operations;
2008-04-17 ago prove_global: pass context;
2008-04-15 ago PureThy.hide_fact;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-03 ago Added skip_mono flag to inductive definition package.
2008-03-29 ago simplified PureThy.store_thm;
2008-03-29 ago eliminated quiete_mode ref (turned into proper argument);
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;