summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/FOL/IFOL.thy

changeset 12937 | 0c4fd7529467 |

parent 12875 | bda60442bf02 |

child 13435 | 05631e8f0258 |

1.1 --- a/src/FOL/IFOL.thy Mon Feb 25 20:46:09 2002 +0100 1.2 +++ b/src/FOL/IFOL.thy Mon Feb 25 20:48:14 2002 +0100 1.3 @@ -126,7 +126,10 @@ 1.4 subsection {* Intuitionistic Reasoning *} 1.5 1.6 lemma impE': 1.7 - (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R 1.8 + assumes 1: "P --> Q" 1.9 + and 2: "Q ==> R" 1.10 + and 3: "P --> Q ==> P" 1.11 + shows R 1.12 proof - 1.13 from 3 and 1 have P . 1.14 with 1 have Q by (rule impE) 1.15 @@ -134,13 +137,18 @@ 1.16 qed 1.17 1.18 lemma allE': 1.19 - (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q 1.20 + assumes 1: "ALL x. P(x)" 1.21 + and 2: "P(x) ==> ALL x. P(x) ==> Q" 1.22 + shows Q 1.23 proof - 1.24 from 1 have "P(x)" by (rule spec) 1.25 from this and 1 show Q by (rule 2) 1.26 qed 1.27 1.28 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R 1.29 +lemma notE': 1.30 + assumes 1: "~ P" 1.31 + and 2: "~ P ==> P" 1.32 + shows R 1.33 proof - 1.34 from 2 and 1 have P . 1.35 with 1 show R by (rule notE)