src/HOL/Tools/function_package/size.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-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-02-09 blanchet 2009-02-09 Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.
2009-02-06 blanchet 2009-02-06 Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-15 haftmann 2009-01-15 tuned
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-09-25 wenzelm 2008-09-25 explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
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-01-10 berghofe 2008-01-10 Now uses more carefully designed simpsets to prevent proofs from failing for some strange datatypes with nested recursion.
2008-01-08 haftmann 2008-01-08 explicit type variables for instantiation
2008-01-05 haftmann 2008-01-05 adhering to instantiation policy
2008-01-02 haftmann 2008-01-02 tuned
2007-12-18 berghofe 2007-12-18 Alternative names are now also used when storing theorems for size functions.
2007-12-17 berghofe 2007-12-17 size functions for nested datatypes are now expressed using generic ..._size functions.
2007-12-07 haftmann 2007-12-07 dropped Instance.instantiate
2007-12-05 haftmann 2007-12-05 canonical instantiation
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-10-23 haftmann 2007-10-23 dropped code redundancy
2007-10-13 wenzelm 2007-10-13 Theory.specify_const: added deps argument;
2007-10-11 wenzelm 2007-10-11 Theory.specify_const;
2007-09-30 wenzelm 2007-09-30 Sign.add_consts_authentic: tags (Markup.property list);
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases; tuned functor application;
2007-09-25 wenzelm 2007-09-25 simplified interpretation setup;
2007-09-25 haftmann 2007-09-25 size hook