src/HOL/Calculation.thy
Mon, 02 Oct 2000 15:13:32 +0200 wenzelm added == transitive rule (bad idea??);
Tue, 01 Aug 2000 00:18:40 +0200 wenzelm tuned;
Sun, 23 Jul 2000 12:01:39 +0200 wenzelm elim?;
Sat, 01 Jul 2000 19:51:08 +0200 wenzelm added subst rules for ord(er), including monotonicity conditions;
Sun, 25 Jun 2000 23:58:54 +0200 wenzelm prefer mp over subst;
Sun, 04 Jun 2000 19:39:29 +0200 wenzelm removed explicit terminator (";");
Wed, 10 May 2000 21:04:16 +0200 wenzelm base on IntArith instead of Int (in order to leave out deleted simproc!);
Sun, 27 Feb 2000 15:21:13 +0100 wenzelm theorems [trans] = rev_mp mp;
Thu, 10 Feb 2000 13:36:23 +0100 wenzelm theorems [elim??] = sym;
Wed, 29 Sep 1999 16:44:18 +0200 wenzelm subsetD;
Tue, 21 Sep 1999 17:28:33 +0200 wenzelm added some ~= rules;
Fri, 27 Aug 1999 20:29:20 +0200 wenzelm tuned;
Mon, 09 Aug 1999 22:25:27 +0200 wenzelm added asym rule;
Fri, 09 Jul 1999 16:45:18 +0200 wenzelm added HOL.trans;
Thu, 01 Jul 1999 17:42:27 +0200 wenzelm tuned;
Wed, 30 Jun 1999 16:00:06 +0200 wenzelm antisym first;
Wed, 30 Jun 1999 13:42:47 +0200 wenzelm more robust trans rules;
Sat, 05 Jun 1999 20:37:29 +0200 wenzelm added Ord.order_antisym;
Fri, 04 Jun 1999 19:57:31 +0200 wenzelm Calculation.thy: Setup transitivity rules for calculational proofs.
less more (0) tip