# HG changeset patch
# User wenzelm
# Date 938803130 -7200
# Node ID 027b6ec2f084f6d85bc2f8bf42e2b5a98402a3fc
# Parent  de2e468a42c84dcb17119d067d61f923ca0f24cc
added 'obtain' command;

diff -r de2e468a42c8 -r 027b6ec2f084 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Oct 01 20:38:16 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 01 20:38:50 1999 +0200
@@ -285,7 +285,7 @@
     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
 
 val thenceP =
-  OuterSyntax.command "thence" "forward chaining, including full export" K.prf_chain
+  OuterSyntax.command "thence" "forward chaining, including full export (EXPERIMENTAL!)" K.prf_chain
     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.export_chain)));
 
 val fromP =
@@ -399,6 +399,18 @@
     (calc_args -- P.marg_comment >> IsarThy.finally);
 
 
+(* obtain *)
+
+val obtainP =
+  OuterSyntax.command "obtain" "document-level existential quantifier (EXPERIMENTAL!)"
+    K.prf_asm_goal
+    (Scan.optional
+      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
+        --| P.$$$ "in") [] --
+      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+    >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
+
+
 (* proof navigation *)
 
 val backP =
@@ -581,8 +593,8 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
-  "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
-  "}"];
+  "concl", "files", "in", "infixl", "infixr", "is", "output", "{",
+  "|", "}"];
 
 val parsers = [
   (*theory structure*)
@@ -601,8 +613,8 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
-  cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
+  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, obtainP,
+  backP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
diff -r de2e468a42c8 -r 027b6ec2f084 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:16 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:50 1999 +0200
@@ -135,6 +135,12 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
+  val obtain: ((string list * string option) * Comment.text) list
+    * ((string * Args.src list * (string * (string list * string list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val obtain_i: ((string list * typ option) * Comment.text) list
+    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val use_mltext: string -> bool -> theory option -> unit
   val use_mltext_theory: string -> bool -> theory -> theory
   val use_setup: string -> theory -> theory
@@ -281,6 +287,9 @@
 
 (* statements *)
 
+fun multi_local_attribute state (name, src, s) =
+  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
+
 local
 
 fun global_statement f (name, src, s) int thy =
@@ -296,8 +305,7 @@
 fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
 
 fun multi_statement f args = ProofHistory.apply (fn state =>
-  f (map (fn (name, src, s) =>
-      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
+  f (map (multi_local_attribute state) args) state);
 
 fun multi_statement_i f args = ProofHistory.apply (f args);
 
@@ -433,6 +441,17 @@
 end;
 
 
+(* obtain *)
+
+fun obtain (xs, asms) = ProofHistory.applys (fn state =>
+  Obtain.obtain (map Comment.ignore xs)
+    (map (multi_local_attribute state o Comment.ignore) asms) state);
+
+fun obtain_i (xs, asms) = ProofHistory.applys
+  (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
+
+
+
 (* use ML text *)
 
 fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;