# HG changeset patch
# User wenzelm
# Date 951661273 -3600
# Node ID d9345bad5e5ce080d892274d06942da53c52f21f
# Parent  4c3f83414de33c5c195c345642eca314626354e1
theorems [trans] = rev_mp mp;

diff -r 4c3f83414de3 -r d9345bad5e5c src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Sun Feb 27 15:15:52 2000 +0100
+++ b/src/HOL/Calculation.thy	Sun Feb 27 15:21:13 2000 +0100
@@ -8,6 +8,7 @@
 
 theory Calculation = Int:;
 
+theorems [trans] = rev_mp mp;
 
 theorem [trans]: "[| s = t; P t |] ==> P s"; 		    (*  =  x  x  *)
   by (rule ssubst);