--- a/src/HOL/Algebra/abstract/Ideal.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML Thu Oct 12 12:16:58 2000 +0200
@@ -166,10 +166,8 @@
Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
by (rtac psubsetI 1);
-by (rtac dvd_imp_subideal 1 THEN atac 1);
-by (rtac contrapos 1); by (assume_tac 1);
-by (rtac subideal_imp_dvd 1);
-by (Asm_simp_tac 1);
+by (etac dvd_imp_subideal 1);
+by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1);
qed "not_dvd_psubideal";
Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))";
--- a/src/HOL/Algebra/abstract/Ring.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML Thu Oct 12 12:16:58 2000 +0200
@@ -140,19 +140,15 @@
qed "uminus_monom";
Goal "!!a::'a::ring. a ~= <0> ==> -a ~= <0>";
-by (etac contrapos 1);
-by (rtac uminus_monom 1);
-by (assume_tac 1);
+by (blast_tac (claset() addIs [uminus_monom]) 1);
qed "uminus_monom_neq";
Goal "!!a::'a::ring. a * b ~= <0> ==> a ~= <0>";
-by (etac contrapos 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
qed "l_nullD";
Goal "!!a::'a::ring. a * b ~= <0> ==> b ~= <0>";
-by (etac contrapos 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
qed "r_nullD";
(* reflection between a = b and a -- b = <0> *)
--- a/src/HOL/Algebra/poly/Degree.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/Algebra/poly/Degree.ML Thu Oct 12 12:16:58 2000 +0200
@@ -30,7 +30,7 @@
qed "deg_aboveI";
Goalw [coeff_def, deg_def]
- "!! p. (n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
+ "(n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
by (case_tac "n = 0" 1);
(* Case n=0 *)
by (Asm_simp_tac 1);
@@ -43,7 +43,7 @@
qed "deg_belowI";
Goalw [coeff_def, deg_def]
- "!! p. deg p < m ==> coeff m p = <0>";
+ "deg p < m ==> coeff m p = <0>";
by (rtac exE 1); (* create !! x. *)
by (rtac boundD 2);
by (assume_tac 3);
@@ -54,13 +54,13 @@
qed "deg_aboveD";
Goalw [deg_def]
- "!! p. deg p = Suc y ==> ~ bound y (Rep_UP p)";
+ "deg p = Suc y ==> ~ bound y (Rep_UP p)";
by (rtac not_less_Least 1);
by (Asm_simp_tac 1);
val lemma1 = result();
Goalw [deg_def, coeff_def]
- "!! p. deg p = Suc y ==> coeff (deg p) p ~= <0>";
+ "deg p = Suc y ==> coeff (deg p) p ~= <0>";
by (rtac classical 1);
by (dtac notnotD 1);
by (cut_inst_tac [("p", "p")] Least_is_bound 1);
@@ -85,8 +85,7 @@
by (assume_tac 1);
val lemma2 = result();
-Goal
- "!! p. deg p ~= 0 ==> coeff (deg p) p ~= <0>";
+Goal "deg p ~= 0 ==> coeff (deg p) p ~= <0>";
by (rtac lemma2 1);
by (Full_simp_tac 1);
by (dtac Suc_pred 1);
@@ -94,8 +93,7 @@
by (Asm_simp_tac 1);
qed "deg_lcoeff";
-Goal
- "!! p. p ~= <0> ==> coeff (deg p) p ~= <0>";
+Goal "p ~= <0> ==> coeff (deg p) p ~= <0>";
by (etac contrapos 1);
by (ftac contrapos2 1);
by (rtac deg_lcoeff 1);
--- a/src/HOL/NumberTheory/EulerFermat.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML Thu Oct 12 12:16:58 2000 +0200
@@ -43,9 +43,7 @@
qed_spec_mp "Bnor_mem_zle";
Goal "a<b ==> b~:BnorRset(a,m)";
-by (res_inst_tac [("Pa","b<=a")] swap 1);
-by (rtac Bnor_mem_zle 2);
-by Auto_tac;
+by (auto_tac (claset() addDs [Bnor_mem_zle], simpset()));
qed "Bnor_mem_zle_swap";
Goal "b:BnorRset(a,m) --> #0<b";
--- a/src/HOL/NumberTheory/IntFact.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/NumberTheory/IntFact.ML Thu Oct 12 12:16:58 2000 +0200
@@ -54,9 +54,7 @@
qed_spec_mp "d22set_le";
Goal "a<b ==> b~:(d22set a)";
-by (res_inst_tac [("Pa","b<=a")] swap 1);
-by (rtac d22set_le 2);
-by Auto_tac;
+by (auto_tac (claset() addDs [d22set_le], simpset()));
qed "d22set_le_swap";
Goal "#1<b --> b<=a --> b:(d22set a)";
--- a/src/HOL/NumberTheory/IntPrimes.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML Thu Oct 12 12:16:58 2000 +0200
@@ -146,12 +146,7 @@
qed "zdvd_zmod_imp_zdvd";
Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)";
-by (zdiv_undefined_case_tac "k=#0" 1);
-by Safe_tac;
-by (res_inst_tac [("x","n div k")] exI 2);
-by (rtac trans 2);
-by (res_inst_tac [("b","k")] zmod_zdiv_equality 2);
-by (ALLGOALS Asm_simp_tac);
+by (auto_tac (claset(), simpset() addsimps [zmod_zmult_self2]));
qed "zdvd_iff_zmod_eq_0";
Goal "[| ~k<#0; k~=#0 |] ==> #0<(k::int)";
@@ -549,12 +544,8 @@
Goal "[| p:zprime; #0<a; a<p; [a*a = #1](mod p) |] ==> a = #1 | a = p-#1";
by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1);
-by Safe_tac;
-by (res_inst_tac [("Pa","a=p-#1")] swap 2);
-by (rtac zcong_zless_imp_eq 1);
-by (rtac zcong_zless_imp_eq 7);
-by (rewtac zprime_def);
-by Auto_tac;
+by (full_simp_tac (simpset() addsimps [zprime_def]) 1);
+by (auto_tac (claset() addIs [zcong_zless_imp_eq], simpset()));
qed "zcong_square_zless";
Goalw [zcong_def] "[| #0<a; a<m; #0<b; b<a |] ==> ~[a = b] (mod m) ";
--- a/src/HOL/ex/set.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOL/ex/set.ML Thu Oct 12 12:16:58 2000 +0200
@@ -58,12 +58,12 @@
Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)";
(*requires best-first search because it is undirectional*)
-by (best_tac (claset() addSEs [equalityCE]) 1);
+by (Best_tac 1);
qed "cantor1";
(*This form displays the diagonal term*)
Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)";
-by (best_tac (claset() addSEs [equalityCE]) 1);
+by (Best_tac 1);
uresult();
(*This form exploits the set constructs*)
@@ -77,7 +77,7 @@
by (assume_tac 1);
choplev 0;
-by (best_tac (claset() addSEs [equalityCE]) 1);
+by (Best_tac 1);
qed "";
--- a/src/HOLCF/Ssum3.ML Thu Oct 12 12:16:22 2000 +0200
+++ b/src/HOLCF/Ssum3.ML Thu Oct 12 12:16:58 2000 +0200
@@ -11,6 +11,8 @@
by (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1);
qed "inst_ssum_pcpo";
+Addsimps [inst_ssum_pcpo RS sym];
+
(* ------------------------------------------------------------------------ *)
(* continuity for Isinl and Isinr *)
(* ------------------------------------------------------------------------ *)
@@ -218,19 +220,12 @@
by (rtac trans 1);
by (rtac cfun_arg_cong 1);
by (rtac Iwhen2 1);
-by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
-by (fast_tac HOL_cs 1);
-by (stac inst_ssum_pcpo 1);
+by (Force_tac 1);
by (res_inst_tac [("t","Y(i)")] ssubst 1);
by (atac 1);
-by (fast_tac HOL_cs 1);
+by Auto_tac;
by (stac Iwhen2 1);
-by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
-by (fast_tac HOL_cs 1);
-by (stac inst_ssum_pcpo 1);
-by (res_inst_tac [("t","Y(i)")] ssubst 1);
-by (atac 1);
-by (fast_tac HOL_cs 1);
+by (Force_tac 1);
by (simp_tac (simpset_of Cfun3.thy) 1);
by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
@@ -274,23 +269,13 @@
by (rtac trans 1);
by (rtac cfun_arg_cong 1);
by (rtac Iwhen3 1);
-by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
-by (fast_tac HOL_cs 1);
-by (dtac notnotD 1);
-by (stac inst_ssum_pcpo 1);
-by (stac strict_IsinlIsinr 1);
+by (Force_tac 1);
by (res_inst_tac [("t","Y(i)")] ssubst 1);
by (atac 1);
-by (fast_tac HOL_cs 1);
by (stac Iwhen3 1);
-by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
-by (fast_tac HOL_cs 1);
-by (dtac notnotD 1);
-by (stac inst_ssum_pcpo 1);
-by (stac strict_IsinlIsinr 1);
+by (Force_tac 1);
by (res_inst_tac [("t","Y(i)")] ssubst 1);
by (atac 1);
-by (fast_tac HOL_cs 1);
by (simp_tac (simpset_of Cfun3.thy) 1);
by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);