summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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