author wenzelm Fri, 27 Aug 1999 20:29:20 +0200 changeset 7381 1bd8633e8f90 parent 7380 2bcee6a460d8 child 7382 33c01075d343
tuned;
 src/HOL/Calculation.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Calculation.thy	Fri Aug 27 18:59:27 1999 +0200
+++ b/src/HOL/Calculation.thy	Fri Aug 27 20:29:20 1999 +0200
@@ -9,33 +9,36 @@
theory Calculation = Int:;

-theorems [trans] = HOL.ssubst;                              (*  =  x  x  *)
-theorems [trans] = HOL.subst[COMP swap_prems_rl];           (*  x  =  x  *)
+theorem [trans]: "[| s = t; P t |] ==> P s"; 		    (*  =  x  x  *)
+  by (rule ssubst);

-theorems [trans] = Divides.dvd_trans;                       (* dvd dvd dvd *)
+theorem [trans]: "[| P s; s = t |] ==> P t";		    (*  x  =  x  *)
+  by (rule subst);
+
+theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)

theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P";   (*  <  >  P  *)
-  by (rule Ord.order_less_asym);
+  by (rule order_less_asym);

-theorems [trans] = Ord.order_less_trans;                    (*  <  <  <  *)
-theorems [trans] = Ord.order_le_less_trans;                 (*  <= <  <  *)
-theorems [trans] = Ord.order_less_le_trans;                 (*  <  <= <  *)
-theorems [trans] = Ord.order_trans;                         (*  <= <= <= *)
-theorems [trans] = Ord.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 HOL.subst);
+  by (rule subst);

theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	    (*  =  <= <= *)
-  by (rule HOL.ssubst);
+  by (rule ssubst);

theorem [trans]: "[| x < y; y = z |] ==> x < z";	    (*  <  =  <  *)
-  by (rule HOL.subst);
+  by (rule subst);

theorem [trans]: "[| x = y; y < z |] ==> x < z";	    (*  =  <  <  *)
-  by (rule HOL.ssubst);
+  by (rule ssubst);

-theorems [trans] = HOL.trans                                (*  =  =  =  *)
+theorems [trans] = trans                                    (*  =  =  =  *)

end;```