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