2009-05-30 ago modernized attribute setup;
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-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago added map_facts_refs;
2009-03-18 ago more precise type Symbol_Pos.text;
2009-03-16 ago tuned signature;
2009-03-15 ago added setup and attribute_setup -- expect plain parser instead of syntax function;
2009-03-13 ago eliminated type Args.T;
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago Thm.binding;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-29 ago Added abs_def attribute.
2009-01-21 ago binding is alias for Binding.T
2008-12-05 ago removed Table.extend, NameSpace.extend_table
2008-12-04 ago cleaned up binding module and related code
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-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-10 ago pass position to get_fact;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-08-06 ago report markup;
2008-08-04 ago tuned signature;
2008-05-14 ago added defined;
2008-04-17 ago no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-16 ago PureThy.get_fact: pass dynamic context;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-20 ago Facts.Named: include position;
2008-03-20 ago renamed former get_thms(_silent) to get_fact(_silent);
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-26 ago misc tuning and internal rearrangement;
2007-09-26 ago added eval_thms;
2007-09-25 ago tuned functor application;
2007-08-13 ago new attribute [rotated]
2007-08-07 ago turned Unify flags into configuration options (global only);
2007-08-02 ago turned simp_depth_limit into configuration option;
2007-08-01 ago tuned config options: eliminated separate attribute "option";
2007-07-28 ago attribute "option": proper naming within the theory
2007-07-28 ago tuned;
2007-07-27 ago renamed Config to ConfigOption;
2007-07-27 ago attribute "option": more elaborate syntax (with value parsing);
2007-07-25 ago added attribute "option" for setting configuration options;
2007-07-23 ago eliminated transform_failure (to avoid critical section for main transactions);
2007-07-08 ago replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 ago avoid polymorphic equality;
2007-05-24 ago tuned Pure/General/name_space.ML
2007-05-10 ago moved conversions to structure Conv;
2007-05-07 ago simplified DataFun interfaces;
2007-04-14 ago Morphism.transform/form;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-01-19 ago removed obsolete Attribute;
2006-12-18 ago switched argument order in *.syntax lifters
2006-12-07 ago thms etc.: proper treatment of internal_fact with selection;
2006-12-05 ago Attrib.internal: morphism;
2006-11-21 ago removed kind attribs;
2006-10-14 ago added pretty_attribs (from attrib.ML);
2006-10-09 ago added kind attributes;