# HG changeset patch
# User wenzelm
# Date 930742967 -7200
# Node ID f80091bdc99206b3ecac50abfb171adbb3579642
# Parent  7f9798c6ca8c476748f79e372d59fb48176ffcdf
more robust trans rules;

diff -r 7f9798c6ca8c -r f80091bdc992 src/HOL/Calculation.thy
--- 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;