propp: 'concl' patterns;
authorwenzelm
Thu Jul 08 18:36:57 1999 +0200 (1999-07-08 ago)
changeset 6936ca17f1b02cde
parent 6935 a3f3f4128cab
child 6937 d9e3e2b30bee
propp: 'concl' patterns;
added 'thence';
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jul 08 18:36:09 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 08 18:36:57 1999 +0200
     1.3 @@ -245,9 +245,7 @@
     1.4  
     1.5  (* statements *)
     1.6  
     1.7 -val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
     1.8 -val propp = P.prop -- Scan.optional is_props [];
     1.9 -fun statement f = (P.opt_thm_name ":" -- propp >> P.triple1) -- P.marg_comment >> f;
    1.10 +fun statement f = (P.opt_thm_name ":" -- P.propp >> P.triple1) -- P.marg_comment >> f;
    1.11  
    1.12  val theoremP =
    1.13    OuterSyntax.command "theorem" "state theorem" K.thy_goal
    1.14 @@ -280,6 +278,10 @@
    1.15    OuterSyntax.command "then" "forward chaining" K.prf_chain
    1.16      (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
    1.17  
    1.18 +val thenceP =
    1.19 +  OuterSyntax.command "thence" "forward chaining, including full export" K.prf_chain
    1.20 +    (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.export_chain)));
    1.21 +
    1.22  val fromP =
    1.23    OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
    1.24      (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
    1.25 @@ -297,12 +299,12 @@
    1.26  
    1.27  val assumeP =
    1.28    OuterSyntax.command "assume" "assume propositions" K.prf_asm
    1.29 -    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
    1.30 +    ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
    1.31        >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
    1.32  
    1.33  val presumeP =
    1.34    OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
    1.35 -    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
    1.36 +    ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
    1.37        >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
    1.38  
    1.39  val fixP =
    1.40 @@ -345,7 +347,7 @@
    1.41  
    1.42  val terminal_proofP =
    1.43    OuterSyntax.command "by" "terminal backward proof" K.qed
    1.44 -    (P.method -- P.interest >> IsarThy.terminal_proof);
    1.45 +    (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
    1.46  
    1.47  val immediate_proofP =
    1.48    OuterSyntax.command "." "immediate proof" K.qed
    1.49 @@ -534,8 +536,8 @@
    1.50  
    1.51  val keywords =
    1.52   ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.53 -  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
    1.54 -  "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.55 +  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "concl",
    1.56 +  "files", "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.57  
    1.58  val parsers = [
    1.59    (*theory structure*)
    1.60 @@ -550,10 +552,10 @@
    1.61    print_ast_translationP, token_translationP, oracleP,
    1.62    (*proof commands*)
    1.63    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.64 -  fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
    1.65 -  qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.66 -  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    1.67 -  cannot_undoP, clear_undoP, redoP, undos_proofP,
    1.68 +  fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
    1.69 +  nextP, qed_withP, qedP, terminal_proofP, immediate_proofP,
    1.70 +  default_proofP, skip_proofP, applyP, then_applyP, proofP, alsoP,
    1.71 +  finallyP, backP, cannot_undoP, clear_undoP, redoP, undos_proofP,
    1.72    kill_proofP, undoP,
    1.73    (*diagnostic commands*)
    1.74    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,