--- a/src/HOL/Calculation.thy Sun Jun 04 00:09:04 2000 +0200
+++ b/src/HOL/Calculation.thy Sun Jun 04 19:39:29 2000 +0200
@@ -6,54 +6,53 @@
list below later rules have priority.
*)
-theory Calculation = IntArith:;
+theory Calculation = IntArith:
-theorems [trans] = rev_mp mp;
+theorems [trans] = rev_mp mp
-theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *)
- by (rule ssubst);
+theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *)
+ by (rule ssubst)
-theorem [trans]: "[| P s; s = t |] ==> P t"; (* x = x *)
- by (rule subst);
+theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *)
+ by (rule subst)
-theorems [trans] = dvd_trans; (* dvd dvd dvd *)
+theorems [trans] = dvd_trans (* dvd dvd dvd *)
-theorem [trans]: "[| c:A; A <= B |] ==> c:B";
- by (rule subsetD);
+theorem [trans]: "[| c:A; A <= B |] ==> c:B"
+ by (rule subsetD)
-theorem [trans]: "[| A <= B; c:A |] ==> c:B";
- by (rule subsetD);
+theorem [trans]: "[| A <= B; c:A |] ==> c:B"
+ by (rule subsetD)
-theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *)
- by (simp! add: order_less_le);
+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"; (* <= ~= < *)
- by (simp! add: order_less_le);
+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 *)
- by (rule order_less_asym);
+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"; (* <= = <= *)
- by (rule subst);
+theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *)
+ by (rule subst)
-theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *)
- by (rule ssubst);
+theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *)
+ by (rule ssubst)
-theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *)
- by (rule subst);
+theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *)
+ by (rule subst)
-theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *)
- by (rule ssubst);
+theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *)
+ by (rule ssubst)
theorems [trans] = trans (* = = = *)
theorems [elim??] = sym
-
-end;
+end