author wenzelm Thu Jul 08 18:36:57 1999 +0200 (1999-07-08 ago) changeset 6936 ca17f1b02cde parent 6935 a3f3f4128cab child 6937 d9e3e2b30bee
propp: 'concl' patterns;
```     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,
```