src/HOL/Calculation.thy
2000-10-23 wenzelm 2000-10-23 tuned;
2000-10-19 wenzelm 2000-10-19 declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-02 wenzelm 2000-10-02 added == transitive rule (bad idea??);
2000-08-01 wenzelm 2000-08-01 tuned;
2000-07-23 wenzelm 2000-07-23 elim?;
2000-07-01 wenzelm 2000-07-01 added subst rules for ord(er), including monotonicity conditions; name all rules; tuned;
2000-06-25 wenzelm 2000-06-25 prefer mp over subst; tuned;
2000-06-04 wenzelm 2000-06-04 removed explicit terminator (";");
2000-05-10 wenzelm 2000-05-10 base on IntArith instead of Int (in order to leave out deleted simproc!);
2000-02-27 wenzelm 2000-02-27 theorems [trans] = rev_mp mp;
2000-02-10 wenzelm 2000-02-10 theorems [elim??] = sym;
1999-09-29 wenzelm 1999-09-29 subsetD;
1999-09-21 wenzelm 1999-09-21 added some ~= rules;
1999-08-27 wenzelm 1999-08-27 tuned;
1999-08-09 wenzelm 1999-08-09 added asym rule;
1999-07-09 wenzelm 1999-07-09 added HOL.trans;
1999-07-01 wenzelm 1999-07-01 tuned;
1999-06-30 wenzelm 1999-06-30 antisym first;
1999-06-30 wenzelm 1999-06-30 more robust trans rules;
1999-06-05 wenzelm 1999-06-05 added Ord.order_antisym;
1999-06-04 wenzelm 1999-06-04 Calculation.thy: Setup transitivity rules for calculational proofs.