# HG changeset patch
# User wenzelm
# Date 930599275 -7200
# Node ID da8a4660fb0cac152a8a506dd1efc0ca181ac10b
# Parent  0b660860c0ade5981c351f4cb9f93b8865f04ed7
added presume command;

diff -r 0b660860c0ad -r da8a4660fb0c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 28 21:47:04 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 28 21:47:55 1999 +0200
@@ -292,6 +292,11 @@
     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
 
+val presumeP =
+  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_decl
+    ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
+      >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
+
 val fixP =
   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
@@ -345,12 +350,12 @@
 
 (* proof steps *)
 
-val refineP =
-  OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
+val applyP =
+  OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
 
-val then_refineP =
-  OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
+val then_applyP =
+  OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
 
 val proofP =
@@ -541,10 +546,10 @@
   print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
-  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
-  thenP, fromP, noteP, beginP, endP, nextP, qed_withP, qedP,
-  terminal_proofP, immediate_proofP, default_proofP, refineP,
-  then_refineP, proofP, alsoP, finallyP, backP, prevP, upP, topP,
+  theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
+  fixP, letP, thenP, fromP, noteP, beginP, endP, nextP, qed_withP,
+  qedP, terminal_proofP, immediate_proofP, default_proofP, applyP,
+  then_applyP, proofP, alsoP, finallyP, backP, prevP, upP, topP,
   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
diff -r 0b660860c0ad -r da8a4660fb0c src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Jun 28 21:47:04 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Jun 28 21:47:55 1999 +0200
@@ -79,6 +79,10 @@
     -> ProofHistory.T -> ProofHistory.T
   val assume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
+  val presume: (string * Args.src list * (string * string list) list) * Comment.text
+    -> ProofHistory.T -> ProofHistory.T
+  val presume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
+    -> ProofHistory.T -> ProofHistory.T
   val show: (string * Args.src list * (string * string list)) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val show_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
@@ -259,8 +263,10 @@
 val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
 val lemma     = global_statement Proof.lemma o Comment.ignore;
 val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
-val assume    = local_statement false Proof.assume I o Comment.ignore;
-val assume_i  = local_statement_i false Proof.assume_i I o Comment.ignore;
+val assume    = local_statement false (Proof.assume assume_tac) I o Comment.ignore;
+val assume_i  = local_statement_i false (Proof.assume_i assume_tac) I o Comment.ignore;
+val presume   = local_statement false (Proof.assume (K all_tac)) I o Comment.ignore;
+val presume_i = local_statement_i false (Proof.assume_i (K all_tac)) I o Comment.ignore;
 val show      = local_statement true Proof.show I o Comment.ignore;
 val show_i    = local_statement_i true Proof.show_i I o Comment.ignore;
 val have      = local_statement true Proof.have I o Comment.ignore;