2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-11 ago prefer plain Attrib.eval_thmss -- also means the assert_forward of Proof.get_thmss_cmd is skipped, leading to uniform (albeit odd) behaviour concerning forward chaining;
2010-05-21 ago print calculation result in the context where the fact is actually defined -- proper externing;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-01 ago adapted Item_Net;
2009-11-01 ago modernized structure Context_Rules;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-17 ago adapted to general Item_Net;
2009-03-15 ago simplified attribute setup;
2009-03-05 ago eliminated obsolete ProofContext.full_bname;
2009-03-01 ago discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-01-21 ago removed Ids;
2009-01-21 ago binding replaces bstring
2008-12-04 ago cleaned up binding module and related code
2008-09-12 ago more procise printing of fact names;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-11 ago Proof.put_thms false;
2007-07-29 ago renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-05-07 ago simplified DataFun interfaces;
2007-04-03 ago avoid clash with Alice keywords;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-11-21 ago renamed Proof.put_thms_internal to Proof.put_thms;
2006-10-09 ago attribute symmetric: zero_var_indexes;
2006-06-12 ago tuned Seq/Envir/Unify interfaces;
2006-02-16 ago Proof.put_thms_internal;
2006-02-06 ago eq_prop: Envir.beta_eta_contract;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-10 ago generic data and attributes;
2005-12-09 ago oriented result pairs in PureThy
2005-11-22 ago Drule.multi_resolves;
2005-09-14 ago tuned;
2005-09-13 ago more self-contained proof elements (material from isar_thy.ML);
2005-06-26 ago export get_calculation;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-05-17 ago tuned;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2004-04-14 ago renamed have_thms to note_thms;
2004-04-13 ago 'also'/'moreover': do not interfere with current facts, allow in chain mode;
2004-04-13 ago fix moreover/this behaviour:
2003-12-06 ago do not reset facts ('this') for moreover and also
2002-07-16 ago avoid "_st" versions of proof data;
2002-01-17 ago Thm.prop_of;
2001-12-06 ago clarified sym_del;
2001-12-05 ago added 'sym' and 'symmetric' atts;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-09 ago theory data: finish method;
2001-11-05 ago pretty/print functions with context;
2001-11-02 ago declare transitive;
2001-10-15 ago tuned NetRules;
2001-02-11 ago more robust selection of calculational rules;
2000-11-16 ago Proof.assert_forward;
2000-09-17 ago Display.pretty_thm_sg;