# HG changeset patch
# User wenzelm
# Date 911210775 -3600
# Node ID c8096461f5c8825c0614811de535bc8cc53ff38c
# Parent  2bded7137593db4f2ffd6c50bdd13c35929166dc
renamed tac / etac to refine / then_refine;

diff -r 2bded7137593 -r c8096461f5c8 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Nov 16 11:05:55 1998 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 16 11:06:15 1998 +0100
@@ -10,7 +10,7 @@
   - have_theorems, have_lemmas;
   - load theory;
   - 'methods' section (proof macros, ML method defs) (!?);
-  - now_block: ProofHistory open / close (!?);
+  - next_block: ProofHistory open / close (!?);
   - from_facts: attribs, args (!?) (beware of termination!!);
 *)
 
@@ -34,7 +34,7 @@
   val qed: ProofHistory.T -> theory
   val kill_proof: ProofHistory.T -> theory
   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
-  val etac: Method.text -> ProofHistory.T -> ProofHistory.T
+  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
@@ -126,7 +126,7 @@
 (* backward steps *)
 
 val tac = ProofHistory.applys o Method.tac;
-val etac = ProofHistory.applys o Method.etac;
+val then_tac = ProofHistory.applys o Method.then_tac;
 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;