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