renamed tac / etac to refine / then_refine;
authorwenzelm
Mon Nov 16 11:06:15 1998 +0100 (1998-11-16 ago)
changeset 5882c8096461f5c8
parent 5881 2bded7137593
child 5883 975c984526b0
renamed tac / etac to refine / then_refine;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Nov 16 11:05:55 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 16 11:06:15 1998 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    - have_theorems, have_lemmas;
     1.5    - load theory;
     1.6    - 'methods' section (proof macros, ML method defs) (!?);
     1.7 -  - now_block: ProofHistory open / close (!?);
     1.8 +  - next_block: ProofHistory open / close (!?);
     1.9    - from_facts: attribs, args (!?) (beware of termination!!);
    1.10  *)
    1.11  
    1.12 @@ -34,7 +34,7 @@
    1.13    val qed: ProofHistory.T -> theory
    1.14    val kill_proof: ProofHistory.T -> theory
    1.15    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.16 -  val etac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.17 +  val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.18    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    1.19    val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    1.20    val trivial_proof: ProofHistory.T -> ProofHistory.T
    1.21 @@ -126,7 +126,7 @@
    1.22  (* backward steps *)
    1.23  
    1.24  val tac = ProofHistory.applys o Method.tac;
    1.25 -val etac = ProofHistory.applys o Method.etac;
    1.26 +val then_tac = ProofHistory.applys o Method.then_tac;
    1.27  val proof = ProofHistory.applys o Method.proof;
    1.28  val end_block = ProofHistory.applys_close Method.end_block;
    1.29  val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;