# HG changeset patch
# User wenzelm
# Date 1129327683 -7200
# Node ID 44b6dde80bf4bbb13424f2cad7410c0071847390
# Parent  9e8ea6058e6416d7352e8050ec5f286db0d369a3
added 'guess';

diff -r 9e8ea6058e64 -r 44b6dde80bf4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Oct 15 00:08:02 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 15 00:08:03 2005 +0200
@@ -433,6 +433,12 @@
         --| P.$$$ "where") [] -- statement
       >> (Toplevel.print oo (Toplevel.proof' o (ProofHistory.apply oo uncurry Obtain.obtain))));
 
+val guessP =
+  OuterSyntax.command "guess" "wild guessing (unstructured)"
+    (K.tag_proof K.prf_asm_goal)
+    (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
+      >> (Toplevel.print oo (Toplevel.proof' o (ProofHistory.applys oo Obtain.guess))));
+
 val letP =
   OuterSyntax.command "let" "bind text variables"
     (K.tag_proof K.prf_decl)
@@ -848,8 +854,8 @@
   print_ast_translationP, token_translationP, oracleP, localeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
-  assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,
-  noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
+  assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
+  withP, noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP,
   default_proofP, immediate_proofP, done_proofP, skip_proofP,
   forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,