src/Pure/Isar/calculation.ML
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;
2000-09-07 wenzelm 2000-09-07 tuned msgs;
2000-07-13 wenzelm 2000-07-13 eq_prop: strip_assums_concl;
2000-07-01 wenzelm 2000-07-01 tuned print_rules;
2000-06-26 wenzelm 2000-06-26 eq_prop: eta contract;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-01 wenzelm 2000-04-01 more robust handling of explicit rules;
2000-03-31 wenzelm 2000-03-31 use Attrib.add_del_args;
2000-03-26 wenzelm 2000-03-26 added 'ultimately';
2000-03-23 wenzelm 2000-03-23 added 'moreover' command;
2000-03-15 wenzelm 2000-03-15 tuned comment;
2000-02-27 wenzelm 2000-02-27 use NetRules;
2000-01-28 wenzelm 2000-01-28 map data;
1999-09-25 wenzelm 1999-09-25 Proof.reset_thms calculationN;
1999-09-21 wenzelm 1999-09-21 differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
1999-09-04 wenzelm 1999-09-04 Library.equal_lists;
1999-09-01 wenzelm 1999-09-01 calculation: thm list; filter differ;
1999-08-09 wenzelm 1999-08-09 append user rules;
1999-07-06 wenzelm 1999-07-06 improved errors;
1999-07-01 wenzelm 1999-07-01 also, finally: opt_rules;
1999-06-05 wenzelm 1999-06-05 tuned;
1999-06-04 wenzelm 1999-06-04 fixed "...": dest_arg;
1999-06-04 wenzelm 1999-06-04 oops;
1999-06-04 wenzelm 1999-06-04 Support for calculational proofs.