src/FOL/IFOL.thy
 changeset 22931 11cc1ccad58e parent 22139 539a63b98f76 child 23155 4b04f9d859af
```--- a/src/FOL/IFOL.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/FOL/IFOL.thy	Fri May 11 00:43:45 2007 +0200
@@ -676,37 +676,37 @@
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
proof
assume "!!x. P(x)"
-  show "ALL x. P(x)" ..
+  then show "ALL x. P(x)" ..
next
assume "ALL x. P(x)"
-  thus "!!x. P(x)" ..
+  then show "!!x. P(x)" ..
qed

lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
proof
assume "A ==> B"
-  thus "A --> B" ..
+  then show "A --> B" ..
next
assume "A --> B" and A
-  thus B by (rule mp)
+  then show B by (rule mp)
qed

lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
proof
assume "x == y"
-  show "x = y" by (unfold prems) (rule refl)
+  show "x = y" unfolding `x == y` by (rule refl)
next
assume "x = y"
-  thus "x == y" by (rule eq_reflection)
+  then show "x == y" by (rule eq_reflection)
qed

lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
proof
assume "A == B"
-  show "A <-> B" by (unfold prems) (rule iff_refl)
+  show "A <-> B" unfolding `A == B` by (rule iff_refl)
next
assume "A <-> B"
-  thus "A == B" by (rule iff_reflection)
+  then show "A == B" by (rule iff_reflection)
qed

lemma atomize_conj [atomize]:```