# HG changeset patch
# User wenzelm
# Date 961970334 -7200
# Node ID d5a841f89e921460285a34300b9155e3f0c0bc3b
# Parent  49f6e45e7199be2e92ed57d52ed5fb16063f6da7
prefer mp over subst;
tuned;

diff -r 49f6e45e7199 -r d5a841f89e92 src/HOL/Calculation.thy
--- 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