# HG changeset patch
# User wenzelm
# Date 970492412 -7200
# Node ID 5a2e00bf1e420feb2bc743b8989e7dd72b7219fa
# Parent  a62b275ac0f7c892a67740bb670ce65498dafa8a
added == transitive rule (bad idea??);

diff -r a62b275ac0f7 -r 5a2e00bf1e42 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Oct 02 15:12:34 2000 +0200
+++ b/src/FOL/FOL.thy	Mon Oct 02 15:13:32 2000 +0200
@@ -79,6 +79,7 @@
   rev_mp
   mp
   trans
+  transitive
 
 lemmas [elim?] = sym
 
diff -r a62b275ac0f7 -r 5a2e00bf1e42 src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Mon Oct 02 15:12:34 2000 +0200
+++ b/src/HOL/Calculation.thy	Mon Oct 02 15:13:32 2000 +0200
@@ -186,6 +186,7 @@
   ord_less_eq_trans
   ord_eq_less_trans
   trans
+  transitive
 
 lemmas [elim?] = sym