--- a/src/HOL/Calculation.thy Wed Jun 30 12:24:32 1999 +0200
+++ b/src/HOL/Calculation.thy Wed Jun 30 13:42:47 1999 +0200
@@ -5,18 +5,30 @@
Setup transitivity rules for calculational proofs.
*)
-theory Calculation = Int:
+theory Calculation = Int:;
-theorems[trans] = HOL.ssubst (* = x x *)
-theorems[trans] = HOL.subst[COMP swap_prems_rl] (* x = x *)
+theorems [trans] = Ord.order_trans; (* <= <= <= *)
+theorems [trans] = Ord.order_less_trans; (* < < < *)
+theorems [trans] = Ord.order_le_less_trans; (* <= < < *)
+theorems [trans] = Ord.order_less_le_trans; (* < <= < *)
+theorems [trans] = Ord.order_antisym; (* <= <= = *)
+
+theorem [trans]: "[| x <= y; y = z |] ==> x <= z";
+ by (rule HOL.subst[with y z]);
-theorems[trans] = Ord.order_trans (* <= <= <= *)
-theorems[trans] = Ord.order_less_trans (* < < < *)
-theorems[trans] = Ord.order_le_less_trans (* <= < < *)
-theorems[trans] = Ord.order_less_le_trans (* < <= < *)
-theorems[trans] = Ord.order_antisym (* <= <= = *)
+theorem [trans]: "[| x = y; y <= z |] ==> x <= z";
+ by (rule HOL.ssubst[with x y]);
+
+theorem [trans]: "[| x < y; y = z |] ==> x < z";
+ by (rule HOL.subst[with y z]);
-theorems[trans] = Divides.dvd_trans (* dvd dvd dvd *)
+theorem [trans]: "[| x = y; y < z |] ==> x < z";
+ by (rule HOL.ssubst[with x y]);
+
+theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *)
+theorems [trans] = HOL.ssubst; (* = x x *)
+
+theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *)
-end
+end;