author wenzelm Sat, 20 Oct 2001 20:18:45 +0200 changeset 11848 6e3017adb8c0 parent 11847 82df5977101b child 11849 53e629437bc8
calculational rules moved from FOL to IFOL;
 src/FOL/FOL.thy file | annotate | diff | comparison | revisions src/FOL/IFOL.thy file | annotate | diff | comparison | revisions
```--- 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```