added presume command;
authorwenzelm
Mon Jun 28 21:47:55 1999 +0200 (1999-06-28 ago)
changeset 6850da8a4660fb0c
parent 6849 0b660860c0ad
child 6851 526c0b90bcef
added presume command;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jun 28 21:47:04 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 28 21:47:55 1999 +0200
     1.3 @@ -292,6 +292,11 @@
     1.4      ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
     1.5        >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
     1.6  
     1.7 +val presumeP =
     1.8 +  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_decl
     1.9 +    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
    1.10 +      >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
    1.11 +
    1.12  val fixP =
    1.13    OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
    1.14      (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
    1.15 @@ -345,12 +350,12 @@
    1.16  
    1.17  (* proof steps *)
    1.18  
    1.19 -val refineP =
    1.20 -  OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
    1.21 +val applyP =
    1.22 +  OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
    1.23      K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
    1.24  
    1.25 -val then_refineP =
    1.26 -  OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
    1.27 +val then_applyP =
    1.28 +  OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
    1.29      K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
    1.30  
    1.31  val proofP =
    1.32 @@ -541,10 +546,10 @@
    1.33    print_translationP, typed_print_translationP,
    1.34    print_ast_translationP, token_translationP, oracleP,
    1.35    (*proof commands*)
    1.36 -  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
    1.37 -  thenP, fromP, noteP, beginP, endP, nextP, qed_withP, qedP,
    1.38 -  terminal_proofP, immediate_proofP, default_proofP, refineP,
    1.39 -  then_refineP, proofP, alsoP, finallyP, backP, prevP, upP, topP,
    1.40 +  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.41 +  fixP, letP, thenP, fromP, noteP, beginP, endP, nextP, qed_withP,
    1.42 +  qedP, terminal_proofP, immediate_proofP, default_proofP, applyP,
    1.43 +  then_applyP, proofP, alsoP, finallyP, backP, prevP, upP, topP,
    1.44    cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.45    (*diagnostic commands*)
    1.46    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Jun 28 21:47:04 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Jun 28 21:47:55 1999 +0200
     2.3 @@ -79,6 +79,10 @@
     2.4      -> ProofHistory.T -> ProofHistory.T
     2.5    val assume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
     2.6      -> ProofHistory.T -> ProofHistory.T
     2.7 +  val presume: (string * Args.src list * (string * string list) list) * Comment.text
     2.8 +    -> ProofHistory.T -> ProofHistory.T
     2.9 +  val presume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
    2.10 +    -> ProofHistory.T -> ProofHistory.T
    2.11    val show: (string * Args.src list * (string * string list)) * Comment.text
    2.12      -> ProofHistory.T -> ProofHistory.T
    2.13    val show_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
    2.14 @@ -259,8 +263,10 @@
    2.15  val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
    2.16  val lemma     = global_statement Proof.lemma o Comment.ignore;
    2.17  val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
    2.18 -val assume    = local_statement false Proof.assume I o Comment.ignore;
    2.19 -val assume_i  = local_statement_i false Proof.assume_i I o Comment.ignore;
    2.20 +val assume    = local_statement false (Proof.assume assume_tac) I o Comment.ignore;
    2.21 +val assume_i  = local_statement_i false (Proof.assume_i assume_tac) I o Comment.ignore;
    2.22 +val presume   = local_statement false (Proof.assume (K all_tac)) I o Comment.ignore;
    2.23 +val presume_i = local_statement_i false (Proof.assume_i (K all_tac)) I o Comment.ignore;
    2.24  val show      = local_statement true Proof.show I o Comment.ignore;
    2.25  val show_i    = local_statement_i true Proof.show_i I o Comment.ignore;
    2.26  val have      = local_statement true Proof.have I o Comment.ignore;