eliminated obsolete aliases;
authorwenzelm
Tue Feb 14 17:11:33 2012 +0100 (2012-02-14)
changeset 4645973823dbbecc4
parent 46458 19ef91d7fbd4
child 46460 68cf3d3550b5
eliminated obsolete aliases;
src/HOL/IMPP/Natural.thy
src/HOL/Set.thy
src/Provers/classical.ML
src/Pure/tactic.ML
     1.1 --- a/src/HOL/IMPP/Natural.thy	Tue Feb 14 16:59:12 2012 +0100
     1.2 +++ b/src/HOL/IMPP/Natural.thy	Tue Feb 14 17:11:33 2012 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
     1.5  apply (erule evalc.induct)
     1.6  apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
     1.7 -apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
     1.8 +apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *})
     1.9  apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
    1.10  done
    1.11  
     2.1 --- a/src/HOL/Set.thy	Tue Feb 14 16:59:12 2012 +0100
     2.2 +++ b/src/HOL/Set.thy	Tue Feb 14 17:11:33 2012 +0100
     2.3 @@ -379,7 +379,7 @@
     2.4  *}
     2.5  
     2.6  declaration {* fn _ =>
     2.7 -  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
     2.8 +  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
     2.9  *}
    2.10  
    2.11  ML {*
     3.1 --- a/src/Provers/classical.ML	Tue Feb 14 16:59:12 2012 +0100
     3.2 +++ b/src/Provers/classical.ML	Tue Feb 14 17:11:33 2012 +0100
     3.3 @@ -670,8 +670,8 @@
     3.4  fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
     3.5  fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
     3.6  
     3.7 -fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
     3.8 -fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
     3.9 +fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
    3.10 +fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
    3.11  fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
    3.12  fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
    3.13  
     4.1 --- a/src/Pure/tactic.ML	Tue Feb 14 16:59:12 2012 +0100
     4.2 +++ b/src/Pure/tactic.ML	Tue Feb 14 17:11:33 2012 +0100
     4.3 @@ -22,9 +22,6 @@
     4.4    val dtac: thm -> int -> tactic
     4.5    val etac: thm -> int -> tactic
     4.6    val ftac: thm -> int -> tactic
     4.7 -  val datac: thm -> int -> int -> tactic
     4.8 -  val eatac: thm -> int -> int -> tactic
     4.9 -  val fatac: thm -> int -> int -> tactic
    4.10    val ares_tac: thm list -> int -> tactic
    4.11    val solve_tac: thm list -> int -> tactic
    4.12    val bimatch_tac: (bool * thm) list -> int -> tactic
    4.13 @@ -140,9 +137,6 @@
    4.14  fun dtac rl = dresolve_tac [rl];
    4.15  fun etac rl = eresolve_tac [rl];
    4.16  fun ftac rl =  forward_tac [rl];
    4.17 -fun datac thm j = EVERY' (dtac thm::replicate j atac);
    4.18 -fun eatac thm j = EVERY' (etac thm::replicate j atac);
    4.19 -fun fatac thm j = EVERY' (ftac thm::replicate j atac);
    4.20  
    4.21  (*Use an assumption or some rules ... A popular combination!*)
    4.22  fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;