# HG changeset patch
# User wenzelm
# Date 931531518 -7200
# Node ID eeeef70c8fe3c41170c497e7ff7bf9a6a6a0c882
# Parent  214e41d27d74e13f43325075520ddfa13ecd2c6e
added HOL.trans;

diff -r 214e41d27d74 -r eeeef70c8fe3 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;