src/HOL/Nominal/nominal_package.ML
2009-06-17 ago datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-06-04 ago avoid Library.foldl_map
2009-03-11 ago HOLogic.mk_set, HOLogic.dest_set
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-06 ago merged
2009-03-05 ago merged
2009-03-05 ago set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
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 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-04 ago cleaned up binding module and related code
2008-11-13 ago Some modifications in code for proving arities to make it work for datatype
2008-11-10 ago Added support for parametric datatypes.
2008-10-22 ago tuned typedef interface
2008-10-19 ago Names of variables in perm_eqs are now chosen more carefully to avoid
2008-09-26 ago Added fresh_star_const.
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
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-07-03 ago Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
2008-06-20 ago DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
2008-06-19 ago removed duplicate of DatatypePackage.read_typ;
2008-06-16 ago allE_Nil: only one copy, proven in regular theory source;
2008-06-11 ago Drule.read_instantiate;
2008-06-10 ago polished interface of datatype package
2008-05-23 ago moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2008-05-22 ago made the naming of the induction principles consistent: weak_induct is
2008-05-07 ago Adapted to encoding of sets as predicates
2008-04-17 ago prove_global: pass context;
2008-04-16 ago Auxiliary permutation functions are no longer declared using add_consts_i,
2008-04-16 ago Adapted to new primrec package.
2008-04-15 ago PureThy.hide_fact;
2008-04-15 ago overloading perm: use big_name;
2008-04-14 ago overloading of perm: adhoc name prevents duplicate fact names;
2008-04-03 ago Added skip_mono flag to inductive definition package.
2008-03-29 ago eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
2008-03-20 ago more antiquotations
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago auxiliary dynamic_thm(s) for fact lookup;
2008-02-25 ago inductive package: simplified group handling;
2008-02-14 ago Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.
2008-01-28 ago Tuned uniqueness proof for recursion combinator.
2008-01-26 ago avoid redundant escaping of Isabelle symbols;
2008-01-26 ago internal inductive: fresh theorem group;
2008-01-24 ago Reimplemented proof of strong induction theorem.
2008-01-03 ago Added function fresh_const.
2007-12-17 ago Deleted copy of indtac.
2007-12-06 ago added new primrec package
2007-10-06 ago simplified interfaces for outer syntax;
2007-10-02 ago inductive: mark internal theorems as Thm.internalK;
2007-09-28 ago Adapted to changes in interface of add_inductive_i.
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-08-28 ago Got rid of large simpset in proof of characteristic equations
2007-08-10 ago ClassPackage renamed to Class
2007-08-01 ago tuned config options: eliminated separate attribute "option";
2007-07-31 ago replaced dtK ref by datatype_distinctness_limit configuration option;
2007-07-05 ago renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;