# HG changeset patch
# User wenzelm
# Date 1007517639 -3600
# Node ID 2af9ad81ea5683d7db98788912e518b3c56a1702
# Parent  1cee8a0db39238c30eee04a8f7b24b5024e355e2
sym declarations;
tuned declarations;

diff -r 1cee8a0db392 -r 2af9ad81ea56 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Dec 05 02:59:49 2001 +0100
+++ b/src/FOL/IFOL.thy	Wed Dec 05 03:00:39 2001 +0100
@@ -117,19 +117,19 @@
 setup Simplifier.setup
 use "IFOL_lemmas.ML"
 
-declare impE [Pure.elim?]  iffD1 [Pure.elim?]  iffD2 [Pure.elim?]
-
 use "fologic.ML"
 use "hypsubstdata.ML"
 setup hypsubst_setup
 use "intprover.ML"
 
 
+subsubsection {* Intuitionistic Reasoning *}
+
 lemma impE':
   (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
 proof -
   from 3 and 1 have P .
-  with 1 have Q ..
+  with 1 have Q by (rule impE)
   with 2 show R .
 qed
 
@@ -156,21 +156,28 @@
 *}
 
 
+lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
+  by rules
+
+lemmas [sym] = sym iff_sym not_sym iff_not_sym
+  and [Pure.elim?] = iffD1 iffD2 impE
+
+
 subsection {* Atomizing meta-level rules *}
 
 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
 proof
   assume "!!x. P(x)"
-  show "ALL x. P(x)" by (rule allI)
+  show "ALL x. P(x)" ..
 next
   assume "ALL x. P(x)"
-  thus "!!x. P(x)" by (rule allE)
+  thus "!!x. P(x)" ..
 qed
 
 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
 proof
-  assume r: "A ==> B"
-  show "A --> B" by (rule impI) (rule r)
+  assume "A ==> B"
+  thus "A --> B" ..
 next
   assume "A --> B" and A
   thus B by (rule mp)
@@ -200,7 +207,7 @@
   qed
 qed
 
-declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
+lemmas [symmetric, rulify] = atomize_all atomize_imp
 
 
 subsection {* Calculational rules *}
@@ -222,6 +229,4 @@
   mp
   trans
 
-lemmas [Pure.elim?] = sym
-
 end