# HG changeset patch
# User paulson
# Date 971345818 -7200
# Node ID 2b255b772585851f58b216e3f9e723dbe5137051
# Parent  4ea3ee8de0198dbabb56f8f7d06bb0a541c53167
tidied

diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/Algebra/abstract/Ideal.ML
--- 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))";
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/Algebra/abstract/Ring.ML
--- 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> *)
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/Algebra/poly/Degree.ML
--- 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);
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/NumberTheory/EulerFermat.ML
--- 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";
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/NumberTheory/IntFact.ML
--- 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)";
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/NumberTheory/IntPrimes.ML
--- 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) ";
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOL/ex/set.ML
--- 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 "";
 
 
diff -r 4ea3ee8de019 -r 2b255b772585 src/HOLCF/Ssum3.ML
--- 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);