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