# 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;