--- a/src/HOL/Calculation.thy Sun Jun 25 23:58:27 2000 +0200
+++ b/src/HOL/Calculation.thy Sun Jun 25 23:58:54 2000 +0200
@@ -8,15 +8,16 @@
theory Calculation = IntArith:
-theorems [trans] = rev_mp mp
-
-theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *)
+theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *)
by (rule ssubst)
-theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *)
+theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *)
by (rule subst)
-theorems [trans] = dvd_trans (* dvd dvd dvd *)
+theorems [trans] = rev_mp mp (* x --> x *)
+ (* --> x x *)
+
+theorems [trans] = dvd_trans (* dvd dvd dvd *)
theorem [trans]: "[| c:A; A <= B |] ==> c:B"
by (rule subsetD)
@@ -24,34 +25,34 @@
theorem [trans]: "[| A <= B; c:A |] ==> c:B"
by (rule subsetD)
-theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y" (* ~= <= < *)
+theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y" (* ~= <= < *)
by (simp! add: order_less_le)
-theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y" (* <= ~= < *)
+theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y" (* <= ~= < *)
by (simp! add: order_less_le)
-theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P" (* < > P *)
+theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P" (* < > P *)
by (rule order_less_asym)
-theorems [trans] = order_less_trans (* < < < *)
-theorems [trans] = order_le_less_trans (* <= < < *)
-theorems [trans] = order_less_le_trans (* < <= < *)
-theorems [trans] = order_trans (* <= <= <= *)
-theorems [trans] = order_antisym (* <= >= = *)
+theorems [trans] = order_less_trans (* < < < *)
+theorems [trans] = order_le_less_trans (* <= < < *)
+theorems [trans] = order_less_le_trans (* < <= < *)
+theorems [trans] = order_trans (* <= <= <= *)
+theorems [trans] = order_antisym (* <= >= = *)
-theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *)
+theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *)
by (rule subst)
-theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *)
+theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *)
by (rule ssubst)
-theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *)
+theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *)
by (rule subst)
-theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *)
+theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *)
by (rule ssubst)
-theorems [trans] = trans (* = = = *)
+theorems [trans] = trans (* = = = *)
theorems [elim??] = sym