--- a/src/Pure/Isar/isar_syn.ML Fri Jul 09 18:47:56 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Jul 09 18:48:33 1999 +0200
@@ -307,6 +307,12 @@
((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
>> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
+val defP =
+ OuterSyntax.command "def" "local definition" K.prf_asm
+ ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
+ (P.$$$ "=" |-- P.termp)) >> P.triple1) -- P.marg_comment
+ >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
+
val fixP =
OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
(Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
@@ -335,12 +341,6 @@
(* end proof *)
-val qed_withP =
- OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
- K.qed_block
- (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
- >> (uncurry IsarThy.global_qed_with));
-
val qedP =
OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
(Scan.option (P.method -- P.interest) >> IsarThy.qed);
@@ -535,9 +535,10 @@
outer_parse.ML, otherwise be prepared for unexpected errors*)
val keywords =
- ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
- "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "concl",
- "files", "infixl", "infixr", "is", "output", "{", "|", "}"];
+ ["!", "!!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<",
+ "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
+ "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
+ "}"];
val parsers = [
(*theory structure*)
@@ -552,11 +553,10 @@
print_ast_translationP, token_translationP, oracleP,
(*proof commands*)
theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
- 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,
+ defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
+ nextP, 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,