# HG changeset patch
# User wenzelm
# Date 1003601925 -7200
# Node ID 6e3017adb8c02eb39291265f58a0863cb0835aaa
# Parent  82df5977101b57b9e67d1235bb9e549e1d12b050
calculational rules moved from FOL to IFOL;

diff -r 82df5977101b -r 6e3017adb8c0 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Oct 20 20:18:19 2001 +0200
+++ b/src/FOL/FOL.thy	Sat Oct 20 20:18:45 2001 +0200
@@ -81,27 +81,4 @@
 
 setup InductMethod.setup
 
-
-subsection {* Calculational rules *}
-
-lemma forw_subst: "a = b ==> P(b) ==> P(a)"
-  by (rule ssubst)
-
-lemma back_subst: "P(a) ==> a = b ==> P(b)"
-  by (rule subst)
-
-text {*
-  Note that this list of rules is in reverse order of priorities.
-*}
-
-lemmas trans_rules [trans] =
-  forw_subst
-  back_subst
-  rev_mp
-  mp
-  transitive
-  trans
-
-lemmas [elim?] = sym
-
 end
diff -r 82df5977101b -r 6e3017adb8c0 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Oct 20 20:18:19 2001 +0200
+++ b/src/FOL/IFOL.thy	Sat Oct 20 20:18:45 2001 +0200
@@ -160,4 +160,27 @@
 
 declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
 
+
+subsection {* Calculational rules *}
+
+lemma forw_subst: "a = b ==> P(b) ==> P(a)"
+  by (rule ssubst)
+
+lemma back_subst: "P(a) ==> a = b ==> P(b)"
+  by (rule subst)
+
+text {*
+  Note that this list of rules is in reverse order of priorities.
+*}
+
+lemmas trans_rules [trans] =
+  forw_subst
+  back_subst
+  rev_mp
+  mp
+  transitive
+  trans
+
+lemmas [Pure.elim] = sym
+
 end