src/Pure/Isar/isar_syn.ML
changeset 6888 d0c68ebdabc5
parent 6886 7d0f7ad5a35f
child 6890 05732285677e
--- a/src/Pure/Isar/isar_syn.ML	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -355,6 +355,10 @@
   OuterSyntax.command ".." "default proof" K.qed
     (Scan.succeed IsarThy.default_proof);
 
+val skip_proofP =
+  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
+    (Scan.succeed IsarThy.skip_proof);
+
 
 (* proof steps *)
 
@@ -560,9 +564,9 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
   qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  applyP, then_applyP, proofP, alsoP, finallyP, backP, prevP, upP,
-  topP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP,
-  undoP,
+  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
+  prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
+  kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,