# HG changeset patch
# User wenzelm
# Date 1138894630 -3600
# Node ID 50a27d7c8951d57e8a90052d72b878bd9773715e
# Parent  f1333b0ff9e53d0b5863ccc0d53551803c4026ba
tuned;

diff -r f1333b0ff9e5 -r 50a27d7c8951 NEWS
--- 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").