# HG changeset patch
# User wenzelm
# Date 916157993 -3600
# Node ID 2c9ed58c30ba7e9ff6988741fb0c043f229aa9ef
# Parent  1418bc571f2312d3322feb0e763d4daccd6b5f95
'same' method, 'immediate' proof;

diff -r 1418bc571f23 -r 2c9ed58c30ba src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 12 17:19:13 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 12 17:19:53 1999 +0100
@@ -353,9 +353,9 @@
 val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
 val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
 
-val trivial_proofP =
-  OuterSyntax.parser false "." "trivial proof"
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.trivial_proof));
+val immediate_proofP =
+  OuterSyntax.parser false "." "immediate proof"
+    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
 
 val default_proofP =
   OuterSyntax.parser false ".." "default proof"
@@ -524,7 +524,7 @@
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
-  then_refineP, proofP, terminal_proofP, trivial_proofP,
+  then_refineP, proofP, terminal_proofP, immediate_proofP,
   default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
   prevP, upP, topP,
   (*diagnostic commands*)
diff -r 1418bc571f23 -r 2c9ed58c30ba src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:13 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:53 1999 +0100
@@ -45,7 +45,7 @@
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
   val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
-  val trivial_proof: ProofHistory.T -> ProofHistory.T
+  val immediate_proof: ProofHistory.T -> ProofHistory.T
   val default_proof: ProofHistory.T -> ProofHistory.T
   val use_mltext: string -> theory option -> theory option
   val use_mltext_theory: string -> theory -> theory
@@ -167,7 +167,7 @@
 val proof = ProofHistory.applys o Method.proof;
 val end_block = ProofHistory.applys_close Method.end_block;
 val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
-val trivial_proof = ProofHistory.applys_close Method.trivial_proof;
+val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
 val default_proof = ProofHistory.applys_close Method.default_proof;
 
 
diff -r 1418bc571f23 -r 2c9ed58c30ba src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jan 12 17:19:13 1999 +0100
+++ b/src/Pure/Isar/method.ML	Tue Jan 12 17:19:53 1999 +0100
@@ -19,7 +19,7 @@
   val METHOD0: tactic -> Proof.method
   val fail: Proof.method
   val succeed: Proof.method
-  val trivial: Proof.method
+  val same: Proof.method
   val assumption: Proof.method
   val forward_chain: thm list -> thm list -> thm Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
@@ -56,7 +56,7 @@
   val proof: text option -> Proof.state -> Proof.state Seq.seq
   val end_block: Proof.state -> Proof.state Seq.seq
   val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
-  val trivial_proof: Proof.state -> Proof.state Seq.seq
+  val immediate_proof: Proof.state -> Proof.state Seq.seq
   val default_proof: Proof.state -> Proof.state Seq.seq
   val qed: bstring option -> theory attribute list option -> Proof.state
     -> theory * (string * string * thm)
@@ -82,15 +82,15 @@
 val succeed = METHOD (K all_tac);
 
 
-(* trivial, assumption *)
+(* same, assumption *)
 
-fun trivial_tac [] = K all_tac
-  | trivial_tac facts =
+fun same_tac [] = K all_tac
+  | same_tac facts =
       let val r = ~ (length facts);
       in metacuts_tac facts THEN' rotate_tac r end;
 
-val trivial = METHOD (ALLGOALS o trivial_tac);
-val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
+val same = METHOD (ALLGOALS o same_tac);
+val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));
 
 val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS assume_tac)));
 
@@ -293,7 +293,7 @@
 val end_block = Proof.end_block (dynamic_method finishN);
 
 fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
-val trivial_proof = terminal_proof (Basic (K trivial));
+val immediate_proof = terminal_proof (Basic (K same));
 val default_proof = terminal_proof default_txt;
 
 val qed = Proof.qed (dynamic_method finishN);
@@ -307,7 +307,7 @@
 val pure_methods =
  [("fail", no_args fail, "force failure"),
   ("succeed", no_args succeed, "succeed"),
-  ("trivial", no_args trivial, "proof all goals trivially"),
+  ("same", no_args same, "insert facts, nothing else"),
   ("assumption", no_args assumption, "proof by assumption"),
   ("finish", no_args asm_finish, "finish proof by assumption"),
   ("rule", thms_args rule, "apply primitive rule")];