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-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-12 ago simplified preparation and outer parsing of specification;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Fix parentheses.
2009-03-04 ago Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-03 ago 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;
2009-01-21 ago binding is alias for Binding.T
2008-12-31 ago qualified Term.rename_wrt_term;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-13 ago Modified nominal_primrec to make it work with local theories, unified syntax
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-10-07 ago arbitrary is undefined
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-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-03-29 ago eliminated quiete_mode ref (unused);
2007-12-06 ago added new primrec package
2007-10-08 ago turned keywords invariant/freshness_context into reserved indentifiers;
2007-10-06 ago simplified interfaces for outer syntax;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-09-25 ago Syntax.parse/check/read;
2007-08-30 ago replaced ProofContext.infer_types by general Syntax.check_terms;
2007-07-11 ago Moved unify_consts to PrimrecPackage.
2007-06-19 ago balanced conjunctions;
2007-06-13 ago Method.Basic: include position;
2007-05-18 ago Fixed bug in subst causing primrec functions returning functions
2007-04-18 ago simplified ProofContext.infer_types(_pats);
2007-04-15 ago removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 ago proper ProofContext.infer_types;
2007-03-10 ago - Replaced fold by fold_rev to make sure that list of predicate
2007-02-16 ago Replaced "raise RecError" by "primrec_err" in function
2007-01-19 ago moved parts of OuterParse to SpecParse;
2006-12-11 ago nominal_primrec now prints initial proof state.
2006-12-01 ago Added missing "standard"
2006-11-27 ago Implemented new "nominal_primrec" command for defining