2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 simplified preparation and outer parsing of specification; export extern cmd interfaces as well;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
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-04 blanchet 2009-03-04 Fix parentheses.
2009-03-04 blanchet 2009-03-04 Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-13 berghofe 2008-12-13 Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
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-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (unused);
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-10-08 wenzelm 2007-10-08 turned keywords invariant/freshness_context into reserved indentifiers;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-08-30 wenzelm 2007-08-30 replaced ProofContext.infer_types by general Syntax.check_terms;
2007-07-11 berghofe 2007-07-11 Moved unify_consts to PrimrecPackage.
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-13 wenzelm 2007-06-13 Method.Basic: include position;
2007-05-18 berghofe 2007-05-18 Fixed bug in subst causing primrec functions returning functions to be rejected.
2007-04-18 wenzelm 2007-04-18 simplified ProofContext.infer_types(_pats);
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-03-10 berghofe 2007-03-10 - Replaced fold by fold_rev to make sure that list of predicate variables pvars (for invariants) is in the correct order - Adapted to new format of datatype descriptor
2007-02-16 berghofe 2007-02-16 Replaced "raise RecError" by "primrec_err" in function gen_primrec_i to prevent error message from being suppressed.
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-12-11 berghofe 2006-12-11 nominal_primrec now prints initial proof state.
2006-12-01 nipkow 2006-12-01 Added missing "standard"
2006-11-27 berghofe 2006-11-27 Implemented new "nominal_primrec" command for defining functions on nominal datatypes.