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