summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 02 Feb 2006 16:37:10 +0100 | |

changeset 18910 | 50a27d7c8951 |

parent 18909 | f1333b0ff9e5 |

child 18911 | 74edab16166f |

tuned;

--- a/NEWS Thu Feb 02 16:31:38 2006 +0100 +++ b/NEWS Thu Feb 02 16:37:10 2006 +0100 @@ -80,7 +80,7 @@ 'shows' (a simultaneous conjunction, as before), or 'obtains' (essentially a disjunction of cases with local parameters and assumptions). The latter allows to express general elimination rules -adequately. In this notation common elimination rules look like this: +adequately; in this notation common elimination rules look like this: lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" assumes "EX x. P x" @@ -96,20 +96,21 @@ A | B -The subsequent classical rules refer to the formal "thesis" +The subsequent classical rules even refer to the formal "thesis" explicitly: lemma classical: -- "(~ thesis ==> thesis) ==> thesis" obtains "~ thesis" - lemma Peirce's_Law: -- "((thesis ==> A) ==> thesis) ==> thesis" - obtains "thesis ==> A" + lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" + obtains "thesis ==> something" The actual proof of an 'obtains' statement is analogous to that of the -Isar 'obtain' element, only that there may be several cases. Optional -case names may be specified in parentheses; these will be also used to -annotate the resulting rule for later use with the 'cases' method -(cf. attribute case_names). +Isar proof element 'obtain', only that there may be several cases. +Optional case names may be specified in parentheses; these will be +available both in the present proof and as annotations in the +resulting rule, for later use with the 'cases' method (cf. attribute +case_names). * Isar: 'obtain' takes an optional case name for the local context introduction rule (default "that").