# HG changeset patch
# User wenzelm
# Date 1434201419 -7200
# Node ID 3a0d57f1d6ef16ea740c360fb86ef1ecf8f43b88
# Parent  1f2b29f7843983a50eb77a0805eeb7f3a6657ee2
tuned comments;

diff -r 1f2b29f78439 -r 3a0d57f1d6ef src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jun 13 14:37:50 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Jun 13 15:16:59 2015 +0200
@@ -1,40 +1,7 @@
 (*  Title:      Pure/Isar/obtain.ML
     Author:     Markus Wenzel, TU Muenchen
 
-The 'obtain' and 'guess' language elements -- generalized existence at
-the level of proof texts: 'obtain' involves a proof that certain
-fixes/assumes may be introduced into the present context; 'guess' is
-similar, but derives these elements from the course of reasoning!
-
-
-  <chain_facts>
-  obtain x where "A x" <proof> ==
-
-  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
-  proof succeed
-    fix thesis
-    assume that [intro?]: "!!x. A x ==> thesis"
-    <chain_facts>
-    show thesis
-      apply (insert that)
-      <proof>
-  qed
-  fix x assm <<obtain_export>> "A x"
-
-
-  <chain_facts>
-  guess x <proof body> <proof end> ==
-
-  {
-    fix thesis
-    <chain_facts> have "PROP ?guess"
-      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
-      <proof body>
-      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
-        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
-      <proof end>
-  }
-  fix x assm <<obtain_export>> "A x"
+Generalized existence and cases rules within Isar proof text.
 *)
 
 signature OBTAIN =
@@ -59,7 +26,9 @@
 structure Obtain: OBTAIN =
 struct
 
-(** obtain_export **)
+(** specification elements **)
+
+(* obtain_export *)
 
 (*
   [x, A x]
@@ -99,9 +68,6 @@
   (eliminate ctxt rule xs As, eliminate_term ctxt xs);
 
 
-
-(** specification elements **)
-
 (* result declaration *)
 
 fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) =
@@ -207,7 +173,23 @@
 
 
 
-(** obtain **)
+(** obtain: augmented context based on generalized existence rule **)
+
+(*
+  <chain_facts>
+  obtain x where "A x" <proof> ==
+
+  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
+  proof succeed
+    fix thesis
+    assume that [intro?]: "!!x. A x ==> thesis"
+    <chain_facts>
+    show thesis
+      apply (insert that)
+      <proof>
+  qed
+  fix x assm <<obtain_export>> "A x"
+*)
 
 local
 
@@ -315,7 +297,23 @@
 
 
 
-(** guess **)
+(** guess: obtain based on tactical result **)
+
+(*
+  <chain_facts>
+  guess x <proof body> <proof end> ==
+
+  {
+    fix thesis
+    <chain_facts> have "PROP ?guess"
+      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
+      <proof body>
+      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
+        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
+      <proof end>
+  }
+  fix x assm <<obtain_export>> "A x"
+*)
 
 local