src/HOL/Calculation.thy

--- a/src/HOL/Calculation.thy	Fri Jul 09 16:44:55 1999 +0200
+++ b/src/HOL/Calculation.thy	Fri Jul 09 16:45:18 1999 +0200
@@ -8,6 +8,7 @@
 
 theory Calculation = Int:;
 
+
 theorems [trans] = HOL.ssubst;                          (*  =  x  x  *)
 theorems [trans] = HOL.subst[COMP swap_prems_rl];       (*  x  =  x  *)
 
@@ -31,5 +32,7 @@
 theorem [trans]: "[| x = y; y < z |] ==> x < z";	(*  =  <  <  *)
   by (rule HOL.ssubst);
 
+theorems [trans] = HOL.trans                            (*  =  =  =  *)
+
 
 end;