equal
deleted
inserted
replaced
756 Outer_Syntax.command @{command_keyword consider} "state cases rule" |
756 Outer_Syntax.command @{command_keyword consider} "state cases rule" |
757 (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); |
757 (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); |
758 |
758 |
759 val _ = |
759 val _ = |
760 Outer_Syntax.command @{command_keyword obtain} "generalized elimination" |
760 Outer_Syntax.command @{command_keyword obtain} "generalized elimination" |
761 (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement |
761 (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement |
762 >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z))); |
762 >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); |
763 |
763 |
764 val _ = |
764 val _ = |
765 Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" |
765 Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" |
766 (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); |
766 (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); |
767 |
767 |