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