equal
deleted
inserted
replaced
434 |
434 |
435 val guessP = |
435 val guessP = |
436 OuterSyntax.command "guess" "wild guessing (unstructured)" |
436 OuterSyntax.command "guess" "wild guessing (unstructured)" |
437 (K.tag_proof K.prf_asm_goal) |
437 (K.tag_proof K.prf_asm_goal) |
438 (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
438 (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
439 >> (Toplevel.print oo (Toplevel.proofs' o Obtain.guess))); |
439 >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); |
440 |
440 |
441 val letP = |
441 val letP = |
442 OuterSyntax.command "let" "bind text variables" |
442 OuterSyntax.command "let" "bind text variables" |
443 (K.tag_proof K.prf_decl) |
443 (K.tag_proof K.prf_decl) |
444 (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term)) |
444 (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term)) |