added 'def';
authorwenzelm
Fri Jul 09 18:48:33 1999 +0200 (1999-07-09 ago)
changeset 6953b3f6c39aaa2e
parent 6952 0f7e8d42902b
child 6954 dbeafc269f4f
added 'def';
added "!!" keyword;
removed 'qed_with';
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jul 09 18:47:56 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 09 18:48:33 1999 +0200
     1.3 @@ -307,6 +307,12 @@
     1.4      ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
     1.5        >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
     1.6  
     1.7 +val defP =
     1.8 +  OuterSyntax.command "def" "local definition" K.prf_asm
     1.9 +    ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
    1.10 +      (P.$$$ "=" |-- P.termp)) >> P.triple1) -- P.marg_comment
    1.11 +      >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
    1.12 +
    1.13  val fixP =
    1.14    OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
    1.15      (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
    1.16 @@ -335,12 +341,6 @@
    1.17  
    1.18  (* end proof *)
    1.19  
    1.20 -val qed_withP =
    1.21 -  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
    1.22 -    K.qed_block
    1.23 -    (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
    1.24 -      >> (uncurry IsarThy.global_qed_with));
    1.25 -
    1.26  val qedP =
    1.27    OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
    1.28      (Scan.option (P.method -- P.interest) >> IsarThy.qed);
    1.29 @@ -535,9 +535,10 @@
    1.30    outer_parse.ML, otherwise be prepared for unexpected errors*)
    1.31  
    1.32  val keywords =
    1.33 - ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.34 -  "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "concl",
    1.35 -  "files", "infixl", "infixr", "is", "output", "{", "|", "}"];
    1.36 + ["!", "!!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<",
    1.37 +  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
    1.38 +  "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
    1.39 +  "}"];
    1.40  
    1.41  val parsers = [
    1.42    (*theory structure*)
    1.43 @@ -552,11 +553,10 @@
    1.44    print_ast_translationP, token_translationP, oracleP,
    1.45    (*proof commands*)
    1.46    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.47 -  fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
    1.48 -  nextP, qed_withP, qedP, terminal_proofP, immediate_proofP,
    1.49 -  default_proofP, skip_proofP, applyP, then_applyP, proofP, alsoP,
    1.50 -  finallyP, backP, cannot_undoP, clear_undoP, redoP, undos_proofP,
    1.51 -  kill_proofP, undoP,
    1.52 +  defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
    1.53 +  nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.54 +  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    1.55 +  cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.56    (*diagnostic commands*)
    1.57    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.58    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,