src/Pure/Isar/isar_syn.ML

 
 (** proof commands **)
 
 (* statements *)
 
-val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
-val propp = P.prop -- Scan.optional is_props [];
-fun statement f = (P.opt_thm_name ":" -- propp >> P.triple1) -- P.marg_comment >> f;
+fun statement f = (P.opt_thm_name ":" -- P.propp >> P.triple1) -- P.marg_comment >> f;
 
 val theoremP =
   OuterSyntax.command "theorem" "state theorem" K.thy_goal
     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
 

 
 val thenP =
   OuterSyntax.command "then" "forward chaining" K.prf_chain
     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
 
+val thenceP =
+  OuterSyntax.command "thence" "forward chaining, including full export" K.prf_chain
+    (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.export_chain)));
+
 val fromP =
   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
 
 val withP =

 
 (* proof context *)
 
 val assumeP =
   OuterSyntax.command "assume" "assume propositions" K.prf_asm
-    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
+    ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
 
 val presumeP =
   OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
-    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
+    ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
 
 val fixP =
   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment

   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
 
 val terminal_proofP =
   OuterSyntax.command "by" "terminal backward proof" K.qed
-    (P.method -- P.interest >> IsarThy.terminal_proof);
+    (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
 
 val immediate_proofP =
   OuterSyntax.command "." "immediate proof" K.qed
     (Scan.succeed IsarThy.immediate_proof);
 

 (*keep keywords consistent with the parsers, including those in
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
  ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
-  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
-  "infixl", "infixr", "is", "output", "{", "|", "}"];
+  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "concl",
+  "files", "infixl", "infixr", "is", "output", "{", "|", "}"];
 
 val parsers = [
   (*theory structure*)
   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   (*theory sections*)

   pathP, useP, mlP, setupP, parse_ast_translationP,
   parse_translationP, print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   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,
-  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
-  cannot_undoP, clear_undoP, redoP, undos_proofP,
+  fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
+  nextP, qed_withP, 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,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   print_thmsP, print_propP, print_termP, print_typeP,