src/Provers/classical.ML
changeset 11181 d04f57b91166
parent 11168 b964accc9307
child 11723 2b4a0d630071
     1.1 --- a/src/Provers/classical.ML	Fri Feb 23 16:31:18 2001 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Feb 23 16:31:21 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  (*higher precedence than := facilitates use of references*)
     1.5  infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules
     1.6    addSWrapper delSWrapper addWrapper delWrapper
     1.7 -  addSbefore addSaltern addbefore addaltern
     1.8 +  addSbefore addSafter addbefore addafter
     1.9    addD2 addE2 addSD2 addSE2;
    1.10  
    1.11  
    1.12 @@ -66,9 +66,9 @@
    1.13    val addWrapper        : claset * (string * wrapper) -> claset
    1.14    val delWrapper        : claset *  string            -> claset
    1.15    val addSbefore        : claset * (string * (int -> tactic)) -> claset
    1.16 -  val addSaltern        : claset * (string * (int -> tactic)) -> claset
    1.17 +  val addSafter         : claset * (string * (int -> tactic)) -> claset
    1.18    val addbefore         : claset * (string * (int -> tactic)) -> claset
    1.19 -  val addaltern         : claset * (string * (int -> tactic)) -> claset
    1.20 +  val addafter          : claset * (string * (int -> tactic)) -> claset
    1.21    val addD2             : claset * (string * thm) -> claset
    1.22    val addE2             : claset * (string * thm) -> claset
    1.23    val addSD2            : claset * (string * thm) -> claset
    1.24 @@ -715,23 +715,23 @@
    1.25  (* compose a safe tactic alternatively before/after safe_step_tac *)
    1.26  fun cs addSbefore  (name,    tac1) =
    1.27      cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
    1.28 -fun cs addSaltern  (name,    tac2) =
    1.29 +fun cs addSafter   (name,    tac2) =
    1.30      cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
    1.31  
    1.32  (*compose a tactic alternatively before/after the step tactic *)
    1.33  fun cs addbefore   (name,    tac1) =
    1.34      cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
    1.35 -fun cs addaltern   (name,    tac2) =
    1.36 +fun cs addafter    (name,    tac2) =
    1.37      cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
    1.38  
    1.39  fun cs addD2     (name, thm) =
    1.40 -    cs addaltern (name, dtac thm THEN' atac);
    1.41 +    cs addafter  (name, datac thm 1);
    1.42  fun cs addE2     (name, thm) =
    1.43 -    cs addaltern (name, etac thm THEN' atac);
    1.44 -fun cs addSD2     (name, thm) =
    1.45 -    cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac);
    1.46 -fun cs addSE2     (name, thm) =
    1.47 -    cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac);
    1.48 +    cs addafter  (name, eatac thm 1);
    1.49 +fun cs addSD2    (name, thm) =
    1.50 +    cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
    1.51 +fun cs addSE2    (name, thm) =
    1.52 +    cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
    1.53  
    1.54  (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
    1.55    Merging the term nets may look more efficient, but the rather delicate