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

src/FOL/IFOL.thy

changeset 12937 | 0c4fd7529467 |

parent 12875 | bda60442bf02 |

child 13435 | 05631e8f0258 |

--- a/src/FOL/IFOL.thy Mon Feb 25 20:46:09 2002 +0100 +++ b/src/FOL/IFOL.thy Mon Feb 25 20:48:14 2002 +0100 @@ -126,7 +126,10 @@ subsection {* Intuitionistic Reasoning *} lemma impE': - (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R + assumes 1: "P --> Q" + and 2: "Q ==> R" + and 3: "P --> Q ==> P" + shows R proof - from 3 and 1 have P . with 1 have Q by (rule impE) @@ -134,13 +137,18 @@ qed lemma allE': - (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q + assumes 1: "ALL x. P(x)" + and 2: "P(x) ==> ALL x. P(x) ==> Q" + shows Q proof - from 1 have "P(x)" by (rule spec) from this and 1 show Q by (rule 2) qed -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R +lemma notE': + assumes 1: "~ P" + and 2: "~ P ==> P" + shows R proof - from 2 and 1 have P . with 1 show R by (rule notE)