# HG changeset patch
# User paulson
# Date 971770843 -7200
# Node ID 5eb935d6cc69cdd3874242e4713f7498ae87b1f2
# Parent  10e2d29a77de03cda6eccf44c414450bb2e3351b
tidying and renaming of contrapos rules

diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -199,8 +199,8 @@
 
 Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}";
 by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1);
-by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
-by (etac contrapos 1);
+by (etac contrapos_pp 1);
+by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
 by (rtac in_pideal_imp_dvd 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("x", "<0>")] exI 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOL/Algebra/abstract/Ring.ML
--- a/src/HOL/Algebra/abstract/Ring.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -308,10 +308,7 @@
 qed "l_integral";
 
 Goal "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
-by (etac contrapos 1);
-by (rtac l_integral 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (blast_tac (claset() addIs [l_integral]) 1); 
 qed "not_integral";
 
 Addsimps [not_integral];
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOL/Algebra/poly/Degree.ML
--- a/src/HOL/Algebra/poly/Degree.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/poly/Degree.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -6,13 +6,9 @@
 
 (* Relating degree and bound *)
 
-goal ProtoPoly.thy
-  "!! f. [| bound m f; f n ~= <0> |] ==> n <= m";
-by (rtac classical 1);
-by (dtac not_leE 1);
-by (dtac boundD 1 THEN atac 1);
-by (etac notE 1);
-by (assume_tac 1);
+Goal "[| bound m f; f n ~= <0> |] ==> n <= m";
+by (force_tac (claset() addDs [inst "m" "n" boundD], 
+               simpset()) 1); 
 qed "below_bound";
 
 goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
@@ -61,7 +57,7 @@
 
 Goalw [deg_def, coeff_def]
   "deg p = Suc y ==> coeff (deg p) p ~= <0>";
-by (rtac classical 1);
+by (rtac ccontr 1);
 by (dtac notnotD 1);
 by (cut_inst_tac [("p", "p")] Least_is_bound 1);
 by (subgoal_tac "bound y (Rep_UP p)" 1);
@@ -94,10 +90,9 @@
 qed "deg_lcoeff";
 
 Goal "p ~= <0> ==> coeff (deg p) p ~= <0>";
-by (etac contrapos 1);
-by (ftac contrapos2 1);
-by (rtac deg_lcoeff 1);
-by (assume_tac 1);
+by (etac contrapos_np 1); 
+by (case_tac "deg p = 0" 1);
+by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
 by (rtac up_eqI 1);
 by (case_tac "n=0" 1);
 by (rotate_tac ~2 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOL/Algebra/poly/PolyRing.ML
--- a/src/HOL/Algebra/poly/PolyRing.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/poly/PolyRing.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -67,30 +67,4 @@
 
 val smult_minus = [smult_l_minus, smult_r_minus];
 
-(* Integrity of smult *)
-(*
-Goal
-  "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
-by (simp_tac (simpset() addsimps [disj_commute]) 1);
-
-by (rtac (disj_commute RS trans) 1);
-by (rtac contrapos2 1);
-by (assume_tac 1);
-by (rtac up_neqI 1);
-by (Full_simp_tac 1);
-by (etac conjE 1);
-by (rtac not_integral 1);
-by (assume_tac 1);
-by (etac contrapos 1);
-back();
-by (rtac up_eqI 1);
-by (Simp_tac 1);
-
-by (rtac integral 1);
-
-by (etac conjE 1);
-
-by (rtac disjCI 1);
-*)
-
 Addsimps [smult_one, smult_l_null, smult_r_null];
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOL/Real/Hyperreal/NSA.ML
--- a/src/HOL/Real/Hyperreal/NSA.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Real/Hyperreal/NSA.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -430,48 +430,48 @@
     simpset()));
 qed "HFinite_sum_squares";
 
-Goal "!!x. x ~: Infinitesimal ==> x ~= 0";
+Goal "x ~: Infinitesimal ==> x ~= 0";
 by (Auto_tac);
 qed "not_Infinitesimal_not_zero";
 
-Goal "!!x. x: HFinite - Infinitesimal ==> x ~= 0";
+Goal "x: HFinite - Infinitesimal ==> x ~= 0";
 by (Auto_tac);
 qed "not_Infinitesimal_not_zero2";
 
-Goal "!!x. x : Infinitesimal ==> abs x : Infinitesimal";
+Goal "x : Infinitesimal ==> abs x : Infinitesimal";
 by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
 qed "Infinitesimal_hrabs";
 
-Goal "!!x. x ~: Infinitesimal ==> abs x ~: Infinitesimal";
+Goal "x ~: Infinitesimal ==> abs x ~: Infinitesimal";
 by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
 by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
 qed "not_Infinitesimal_hrabs";
 
-Goal "!!x. abs x : Infinitesimal ==> x : Infinitesimal";
+Goal "abs x : Infinitesimal ==> x : Infinitesimal";
 by (rtac ccontr 1);
 by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1);
 qed "hrabs_Infinitesimal_Infinitesimal";
 
-Goal "!!x. x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
+Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
 by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1);
 qed "HFinite_diff_Infinitesimal_hrabs";
 
 Goalw [Infinitesimal_def] 
-      "!!x. [| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
+      "[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
 by (auto_tac (claset() addSDs [bspec],simpset()));
 by (dres_inst_tac [("i","e")] (hrabs_ge_self RS hypreal_le_less_trans) 1);
 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
 qed "hrabs_less_Infinitesimal";
 
 Goal 
- "!!x. [| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
+ "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
 by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq] addIs
     [hrabs_Infinitesimal_Infinitesimal,hrabs_less_Infinitesimal]) 1);
 qed "hrabs_le_Infinitesimal";
 
 Goalw [Infinitesimal_def] 
-      "!!x. [| e : Infinitesimal; \
+      "[| e : Infinitesimal; \
 \              e' : Infinitesimal; \
 \              e' < x ; x < e |] ==> x : Infinitesimal";
 by (auto_tac (claset() addSDs [bspec],simpset()));
@@ -524,12 +524,12 @@
     addSEs [(hypreal_zero_less_one RSN (2,impE))]) 1);
 qed "Infinitesimal_subset_HFinite";
 
-Goal "!!x. x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
+Goal "x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
 by (etac (HFinite_hypreal_of_real RSN 
           (2,Infinitesimal_HFinite_mult)) 1);
 qed "Infinitesimal_hypreal_of_real_mult";
 
-Goal "!!x. x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
+Goal "x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
 by (etac (HFinite_hypreal_of_real RSN 
           (2,Infinitesimal_HFinite_mult2)) 1);
 qed "Infinitesimal_hypreal_of_real_mult2";
@@ -657,7 +657,7 @@
 by (Asm_simp_tac 1);
 qed "inf_close_eq_imp";
 
-Goal "!!x. x: Infinitesimal ==> -x @= x"; 
+Goal "x: Infinitesimal ==> -x @= x"; 
 by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD1,
     mem_infmal_iff RS iffD1,inf_close_trans2]) 1);
 qed "Infinitesimal_minus_inf_close";
@@ -671,7 +671,7 @@
     bex_Infinitesimal_iff RS sym]) 1);
 qed "bex_Infinitesimal_iff2";
 
-Goal "!!x. [| y: Infinitesimal; x + y = z |] ==> x @= z";
+Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z";
 by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
 by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
@@ -695,13 +695,13 @@
     Infinitesimal_minus_iff RS iffD1]) 1);
 qed "Infinitesimal_add_minus_inf_close_self";
 
-Goal "!!x. [| y: Infinitesimal; x+y @= z|] ==> x @= z";
+Goal "[| y: Infinitesimal; x+y @= z|] ==> x @= z";
 by (dres_inst_tac [("x","x")] (Infinitesimal_add_inf_close_self RS inf_close_sym) 1);
 by (etac (inf_close_trans3 RS inf_close_sym) 1);
 by (assume_tac 1);
 qed "Infinitesimal_add_cancel";
 
-Goal "!!x. [| y: Infinitesimal; x @= z + y|] ==> x @= z";
+Goal "[| y: Infinitesimal; x @= z + y|] ==> x @= z";
 by (dres_inst_tac [("x","z")] (Infinitesimal_add_inf_close_self2  RS inf_close_sym) 1);
 by (etac (inf_close_trans3 RS inf_close_sym) 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
@@ -746,7 +746,7 @@
 
 Addsimps [inf_close_add_right_iff];
 
-Goal "!!x. [| x: HFinite; x @= y |] ==> y: HFinite";
+Goal "[| x: HFinite; x @= y |] ==> y: HFinite";
 by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
 by (Step_tac 1);
 by (dtac (Infinitesimal_subset_HFinite RS subsetD 
@@ -755,7 +755,7 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
 qed "inf_close_HFinite";
 
-Goal "!!x. x @= hypreal_of_real D ==> x: HFinite";
+Goal "x @= hypreal_of_real D ==> x: HFinite";
 by (rtac (inf_close_sym RSN (2,inf_close_HFinite)) 1);
 by (Auto_tac);
 qed "inf_close_hypreal_of_real_HFinite";
@@ -864,18 +864,18 @@
 by (simp_tac (simpset() addsimps [SReal_zero]) 1);
 qed "zero_mem_SReal_Int_Infinitesimal";
 
-Goal "!!x. [| x: SReal; x: Infinitesimal|] ==> x = 0";
+Goal "[| x: SReal; x: Infinitesimal|] ==> x = 0";
 by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "SReal_Infinitesimal_zero";
 
-Goal "!!x. [| x : SReal; x ~= 0 |] \
+Goal "[| x : SReal; x ~= 0 |] \
 \              ==> x : HFinite - Infinitesimal";
 by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
           SReal_subset_HFinite RS subsetD],simpset()));
 qed "SReal_HFinite_diff_Infinitesimal";
 
-Goal "!!x. hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
+Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
 by (rtac SReal_HFinite_diff_Infinitesimal 1);
 by (Auto_tac);
 qed "hypreal_of_real_HFinite_diff_Infinitesimal";
@@ -891,19 +891,19 @@
 qed "hypreal_one_not_Infinitesimal";
 Addsimps [hypreal_one_not_Infinitesimal];
 
-Goal "!!x. [| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
+Goal "[| y: SReal; x @= y; y~= 0 |] ==> x ~= 0";
 by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
 by (blast_tac (claset() addDs 
     [inf_close_sym RS (mem_infmal_iff RS iffD2),
      SReal_not_Infinitesimal,SReal_minus_not_Infinitesimal]) 1);
 qed "inf_close_SReal_not_zero";
 
-Goal "!!x. [| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
+Goal "[| x @= hypreal_of_real y; hypreal_of_real y ~= 0 |] ==> x ~= 0";
 by (rtac inf_close_SReal_not_zero 1);
 by (Auto_tac);
 qed "inf_close_hypreal_of_real_not_zero";
 
-Goal "!!x. [| x @= y; y : HFinite - Infinitesimal |] \
+Goal "[| x @= y; y : HFinite - Infinitesimal |] \
 \                  ==> x : HFinite - Infinitesimal";
 by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
     simpset() addsimps [mem_infmal_iff]));
@@ -911,7 +911,7 @@
 by (blast_tac (claset() addDs [inf_close_sym]) 1);
 qed "HFinite_diff_Infinitesimal_inf_close";
 
-Goal "!!x. [| y ~= 0; y: Infinitesimal; \
+Goal "[| y ~= 0; y: Infinitesimal; \
 \                 x*hrinv(y) : HFinite \
 \              |] ==> x : Infinitesimal";
 by (dtac Infinitesimal_HFinite_mult2 1);
@@ -928,7 +928,7 @@
          Uniqueness: Two infinitely close reals are equal
  ------------------------------------------------------------------*)
 
-Goal "!!x. [|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
+Goal "[|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
 by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
 by (rewrite_goals_tac [inf_close_def]);
 by (dres_inst_tac [("x","y")] SReal_minus 1);
@@ -961,14 +961,14 @@
                 addSDs [isLub_le_isUb]) 1);
 qed "hypreal_isLub_unique";
 
-Goal "!!x. x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
+Goal "x: HFinite ==> EX u. isUb SReal {s. s: SReal & s < x} u";
 by (dtac HFiniteD 1 THEN Step_tac 1);
 by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
 by (auto_tac (claset() addIs [hypreal_less_imp_le,setleI,isUbI,
     hypreal_less_trans],simpset() addsimps [hrabs_interval_iff]));
 qed "lemma_st_part_ub";
 
-Goal "!!x. x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
+Goal "x: HFinite ==> EX y. y: {s. s: SReal & s < x}";
 by (dtac HFiniteD 1 THEN Step_tac 1);
 by (dtac SReal_minus 1);
 by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
@@ -978,7 +978,7 @@
 by (Auto_tac);
 qed "lemma_st_part_subset";
 
-Goal "!!x. x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
+Goal "x: HFinite ==> EX t. isLub SReal {s. s: SReal & s < x} t";
 by (blast_tac (claset() addSIs [SReal_complete,lemma_st_part_ub,
     lemma_st_part_nonempty, lemma_st_part_subset]) 1);
 qed "lemma_st_part_lub";
@@ -990,7 +990,7 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
 qed "lemma_hypreal_le_left_cancel";
 
-Goal "!!x. [| x: HFinite; \
+Goal "[| x: HFinite; \
 \                 isLub SReal {s. s: SReal & s < x} t; \
 \                 r: SReal; 0 < r \
 \              |] ==> x <= t + r";
@@ -1013,7 +1013,7 @@
 by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
 qed "hypreal_gt_isUb";
 
-Goal "!!x. [| x: HFinite; x < y; y: SReal |] \
+Goal "[| x: HFinite; x < y; y: SReal |] \
 \              ==> isUb SReal {s. s: SReal & s < x} y";
 by (auto_tac (claset() addDs [hypreal_less_trans]
     addIs [hypreal_less_imp_le] addSIs [isUbI,setleI],simpset()));
@@ -1241,20 +1241,20 @@
     simpset() addsimps [hypreal_mult_assoc]));
 qed "inf_close_hrinv";
 
-Goal "!!x. [| x: HFinite - Infinitesimal; \
+Goal "[| x: HFinite - Infinitesimal; \
 \                     h : Infinitesimal |] ==> hrinv(x + h) @= hrinv x";
 by (auto_tac (claset() addIs [inf_close_hrinv,
     Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
 qed "hrinv_add_Infinitesimal_inf_close";
 
-Goal "!!x. [| x: HFinite - Infinitesimal; \
+Goal "[| x: HFinite - Infinitesimal; \
 \                     h : Infinitesimal |] ==> hrinv(h + x) @= hrinv x";
 by (rtac (hypreal_add_commute RS subst) 1);
 by (blast_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close]) 1);
 qed "hrinv_add_Infinitesimal_inf_close2";
 
 Goal 
-     "!!x. [| x: HFinite - Infinitesimal; \
+     "[| x: HFinite - Infinitesimal; \
 \             h : Infinitesimal |] ==> hrinv(x + h) + -hrinv x @= h"; 
 by (rtac inf_close_trans2 1);
 by (auto_tac (claset() addIs [hrinv_add_Infinitesimal_inf_close,
@@ -1506,7 +1506,7 @@
 Goalw [hypreal_le_def]
       "[| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
 \      ==> hypreal_of_real x <= hypreal_of_real y";
-by (EVERY1[rtac notI, rtac swap, assume_tac]);
+by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
 by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
 by (auto_tac (claset() addDs [Infinitesimal_minus_iff RS iffD1]
     addIs [Infinitesimal_add_hypreal_of_real_less],
@@ -1523,7 +1523,7 @@
       "!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
 \               hypreal_of_real x + xa <= hypreal_of_real y + ya \
 \            |] ==> hypreal_of_real x <= hypreal_of_real y";
-by (EVERY1[rtac notI, rtac swap, assume_tac]);
+by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
 by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
 by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
 by (dtac Infinitesimal_add 1 THEN assume_tac 1);
@@ -1545,7 +1545,7 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
 qed "hypreal_of_real_less_Infinitesimal_le_zero";
 
-Goal "!!x. [| h: Infinitesimal; x ~= 0 |] \
+Goal "[| h: Infinitesimal; x ~= 0 |] \
 \                  ==> hypreal_of_real x + h ~= 0";
 by (res_inst_tac [("t","h")] (hypreal_minus_minus RS subst) 1);
 by (rtac (not_sym RS (hypreal_not_eq_minus_iff RS iffD1)) 1);
@@ -1687,7 +1687,7 @@
                st_eq_inf_close]) 1);
 qed "st_eq_inf_close_iff";
 
-Goal "!!x. [| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
+Goal "[| x: SReal; e: Infinitesimal |] ==> st(x + e) = x";
 by (forward_tac [st_SReal_eq RS subst] 1);
 by (assume_tac 2);
 by (forward_tac [SReal_subset_HFinite RS subsetD] 1);
@@ -1744,7 +1744,7 @@
 by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
 qed "st_minus";
 
-Goal "!!x. [| x: HFinite; y: HFinite |] \
+Goal "[| x: HFinite; y: HFinite |] \
 \              ==> st (x + -y) = st(x) + -st(y)";
 by (forw_inst_tac [("y1","y")] (st_minus RS sym) 1);
 by (dres_inst_tac [("x1","y")] (HFinite_minus_iff RS iffD1) 1);
@@ -1752,7 +1752,7 @@
 qed "st_add_minus";
 
 (* lemma *)
-Goal "!!x. [| x: HFinite; y: HFinite; \
+Goal "[| x: HFinite; y: HFinite; \
 \                 e: Infinitesimal; \
 \                 ea : Infinitesimal \
 \              |] ==> e*y + x*ea + e*ea: Infinitesimal";
@@ -1763,7 +1763,7 @@
     simpset() addsimps hypreal_add_ac @ hypreal_mult_ac));
 qed "lemma_st_mult";
 
-Goal "!!x. [| x: HFinite; y: HFinite |] \
+Goal "[| x: HFinite; y: HFinite |] \
 \              ==> st (x * y) = st(x) * st(y)";
 by (forward_tac [HFinite_st_Infinitesimal_add] 1);
 by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
@@ -1788,7 +1788,7 @@
 by (fast_tac (claset() addIs [st_zero]) 1);
 qed "st_not_zero";
 
-Goal "!!x. x: Infinitesimal ==> st x = 0";
+Goal "x: Infinitesimal ==> st x = 0";
 by (rtac (st_zero RS subst) 1);
 by (rtac inf_close_st_eq 1);
 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite 
@@ -1814,7 +1814,7 @@
     st_mult,prem2,st_not_Infinitesimal,HFinite_hrinv,prem1,st_hrinv]));
 qed "st_mult_hrinv";
 
-Goal "!!x. x: HFinite ==> st(st(x)) = st(x)";
+Goal "x: HFinite ==> st(st(x)) = st(x)";
 by (blast_tac (claset() addIs [st_HFinite,
     st_inf_close_self,inf_close_st_eq]) 1);
 qed "st_idempotent";
@@ -1877,7 +1877,7 @@
    Alternative definitions for HFinite using Free ultrafilter
  --------------------------------------------------------------------*)
 
-Goal "!!x. [| X: Rep_hypreal x; Y: Rep_hypreal x |] \
+Goal "[| X: Rep_hypreal x; Y: Rep_hypreal x |] \
 \              ==> {n. X n = Y n} : FreeUltrafilterNat";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (Auto_tac);
@@ -1949,7 +1949,7 @@
   Exclude this type of sets from free 
   ultrafilter for Infinite numbers!
  -------------------------------------*)
-Goal "!!x. [| xa: Rep_hypreal x; \
+Goal "[| xa: Rep_hypreal x; \
 \                 {n. abs (xa n) = u} : FreeUltrafilterNat \
 \              |] ==> x: HFinite";
 by (rtac FreeUltrafilterNat_HFinite 1);
@@ -1987,7 +1987,7 @@
 by (auto_tac (claset() addIs [real_less_asym],simpset()));
 qed "lemma_Int_HIa";
 
-Goal "!!x. EX X: Rep_hypreal x. ALL u. \
+Goal "EX X: Rep_hypreal x. ALL u. \
 \              {n. u < abs (X n)}: FreeUltrafilterNat\
 \              ==>  x : HInfinite";
 by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
@@ -2021,7 +2021,7 @@
 qed "lemma_free5";
 
 Goalw [Infinitesimal_def] 
-          "!!x. x : Infinitesimal ==> EX X: Rep_hypreal x. \
+          "x : Infinitesimal ==> EX X: Rep_hypreal x. \
 \          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat";
 by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -2036,7 +2036,7 @@
 qed "Infinitesimal_FreeUltrafilterNat";
 
 Goalw [Infinitesimal_def] 
-          "!!x. EX X: Rep_hypreal x. \
+          "EX X: Rep_hypreal x. \
 \               ALL u. 0 < u --> \
 \               {n. abs (X n) < u}:  FreeUltrafilterNat \
 \               ==> x : Infinitesimal";
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Cfun3.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -335,8 +335,7 @@
 
 
 Goal "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU";
-by (etac swap 1);
-by (dtac notnotD 1);
+by (etac contrapos_nn 1);
 by (dres_inst_tac [("f","ab")] cfun_arg_cong 1);
 by (etac box_equals 1);
 by (fast_tac HOL_cs 1);
@@ -345,8 +344,7 @@
 qed "isorep_defined";
 
 Goal "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU";
-by (etac swap 1);
-by (dtac notnotD 1);
+by (etac contrapos_nn 1);
 by (dres_inst_tac [("f","rep")] cfun_arg_cong 1);
 by (etac box_equals 1);
 by (fast_tac HOL_cs 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Fix.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -367,7 +367,7 @@
 (* an admissible formula is also weak admissible                            *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [admw_def] "!!P. adm(P)==>admw(P)";
+Goalw [admw_def] "adm(P)==>admw(P)";
 by (strip_tac 1);
 by (etac admD 1);
 by (rtac chain_iterate 1);
@@ -483,7 +483,7 @@
 qed "adm_less";
 Addsimps [adm_less];
 
-Goal   "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)";
+Goal   "[| adm P; adm Q |] ==> adm(%x. P x & Q x)";
 by (fast_tac (HOL_cs addEs [admD] addIs [admI]) 1);
 qed "adm_conj";
 Addsimps [adm_conj];
@@ -493,9 +493,9 @@
 qed "adm_not_free";
 Addsimps [adm_not_free];
 
-Goalw [adm_def] "!!t. cont t ==> adm(%x.~ (t x) << u)";
+Goalw [adm_def] "cont t ==> adm(%x.~ (t x) << u)";
 by (strip_tac 1);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
 by (etac spec 1);
 by (rtac trans_less 1);
 by (atac 2);
@@ -504,13 +504,13 @@
 by (atac 1);
 qed "adm_not_less";
 
-Goal   "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)";
+Goal   "!y. adm(P y) ==> adm(%x.!y. P y x)";
 by (fast_tac (HOL_cs addIs [admI] addEs [admD]) 1);
 qed "adm_all";
 
 bind_thm ("adm_all2", allI RS adm_all);
 
-Goal   "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))";
+Goal   "[|cont t; adm P|] ==> adm(%x. P (t x))";
 by (rtac admI 1);
 by (stac (cont2contlub RS contlubE RS spec RS mp) 1);
 by (atac 1);
@@ -528,7 +528,7 @@
 
 Goalw [adm_def] "cont(t)==> adm(%x.~ (t x) = UU)";
 by (strip_tac 1);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
 by (etac spec 1);
 by (rtac (chain_UU_I RS spec) 1);
 by (etac (cont2mono RS ch2ch_monofun) 1);
@@ -678,7 +678,7 @@
 by (atac 1);
 qed "adm_lemma11";
 
-Goal   "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)";
+Goal "[| adm P; adm Q |] ==> adm(%x. P x | Q x)";
 by (rtac admI 1);
 by (rtac (adm_disj_lemma1 RS disjE) 1);
 by (atac 1);
@@ -696,7 +696,7 @@
 bind_thm("adm_lemma11",adm_lemma11);
 bind_thm("adm_disj",adm_disj);
 
-Goal   "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
+Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
 by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
 by (etac ssubst 1);
 by (etac adm_disj 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -451,8 +451,7 @@
 qed"FiniteConcUU1";
 
 Goal "~ Finite ((x::'a Seq)@@UU)";
-by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
-by Auto_tac;
+by (auto_tac (claset() addDs [FiniteConcUU1], simpset()));
 qed"FiniteConcUU";
 
 finiteR_mksch
@@ -968,10 +967,10 @@
 by (subgoal_tac "schB=UU" 1);
 by (Asm_simp_tac 1);
 (* first side: mksch = UU *)
-by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
-                                           (finiteR_mksch RS mp COMP rev_contrapos),
-                                            ForallAnBmksch],
-                           simpset())) 1);
+by (force_tac (claset() addSIs [ForallQFilterPUU,
+                                (finiteR_mksch RS mp COMP rev_contrapos),
+                                  ForallAnBmksch],
+               simpset()) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Sprod0.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -87,7 +87,7 @@
 
 Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU";
 by (rtac (de_Morgan_disj RS subst) 1);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
 by (etac strict_Ispair 1);
 qed "strict_Ispair_rev";
 
@@ -101,7 +101,7 @@
 qed "defined_Ispair_rev";
 
 Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)";
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
 by (etac defined_Ispair_rev 2);
 by (rtac (de_Morgan_disj RS iffD2) 1);
 by (etac conjI 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Sprod3.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -195,7 +195,7 @@
 by (rtac chain_UU_I_inverse 1);
 by (rtac allI 1);
 by (rtac strict_Isfst 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
 by (etac (defined_IsfstIssnd RS conjunct2) 2);
 by (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
 qed "contlub_Isfst";
@@ -214,7 +214,7 @@
 by (rtac chain_UU_I_inverse 1);
 by (rtac allI 1);
 by (rtac strict_Issnd 1);
-by (rtac swap 1);
+by (rtac contrapos_np 1);
 by (etac (defined_IsfstIssnd RS conjunct1) 2);
 by (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS chain_UU_I RS spec]) 1);
 qed "contlub_Issnd";
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Ssum0.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -11,17 +11,11 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
-by (rtac CollectI 1);
-by (rtac disjI1 1);
-by (rtac exI 1);
-by (rtac refl 1);
+by (Blast_tac 1);
 qed "SsumIl";
 
 Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
-by (rtac CollectI 1);
-by (rtac disjI2 1);
-by (rtac exI 1);
-by (rtac refl 1);
+by (Blast_tac 1);
 qed "SsumIr";
 
 Goal "inj_on Abs_Ssum Ssum";
@@ -129,16 +123,14 @@
 by (rtac SsumIr 1);
 qed "inject_Isinr";
 
+AddSDs [inject_Isinl, inject_Isinr];
+
 Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
-by (rtac contrapos 1);
-by (etac inject_Isinl 2);
-by (atac 1);
+by (Blast_tac 1);
 qed "inject_Isinl_rev";
 
 Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
-by (rtac contrapos 1);
-by (etac inject_Isinr 2);
-by (atac 1);
+by (Blast_tac 1);
 qed "inject_Isinr_rev";
 
 (* ------------------------------------------------------------------------ *)
@@ -159,9 +151,9 @@
 by (rtac conjI 1);
 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
 by (etac arg_cong 1);
-by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1);
+by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
 by (etac arg_cong 2);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
 by (rtac trans 1);
 by (etac arg_cong 1);
@@ -175,10 +167,10 @@
 by (rtac conjI 1);
 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
 by (etac arg_cong 1);
-by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1);
+by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
 by (hyp_subst_tac 2);
 by (rtac (strict_SinlSinr_Rep RS sym) 2);
-by (etac contrapos 1);
+by (etac contrapos_nn 1);
 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
 by (rtac trans 1);
 by (etac arg_cong 1);
@@ -262,7 +254,7 @@
 by (strip_tac 1);
 by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
 by (fast_tac HOL_cs  2);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
 by (etac noteq_IsinlIsinr 2);
 by (fast_tac HOL_cs  1);
 qed "Iwhen2";
@@ -282,7 +274,7 @@
 by (strip_tac 1);
 by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
 by (fast_tac HOL_cs  2);
-by (rtac contrapos 1);
+by (rtac contrapos_nn 1);
 by (etac (sym RS noteq_IsinlIsinr) 2);
 by (fast_tac HOL_cs  1);
 by (strip_tac 1);
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Ssum3.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -205,7 +205,7 @@
 by (atac 2);
 by (rtac chain_UU_I_inverse2 1);
 by (stac inst_ssum_pcpo 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (rtac inject_Isinl 1);
 by (rtac trans 1);
 by (etac sym 1);
@@ -253,7 +253,7 @@
 by (atac 2);
 by (rtac chain_UU_I_inverse2 1);
 by (stac inst_ssum_pcpo 1);
-by (etac swap 1);
+by (etac contrapos_np 1);
 by (rtac inject_Isinr 1);
 by (rtac trans 1);
 by (etac sym 1);
@@ -323,50 +323,44 @@
 by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1);
 by (rtac (inst_ssum_pcpo RS sym) 1);
 qed "strict_sinl";
+Addsimps [strict_sinl];
 
 Goalw [sinr_def] "sinr`UU=UU";
 by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1);
 by (rtac (inst_ssum_pcpo RS sym) 1);
 qed "strict_sinr";
+Addsimps [strict_sinr];
 
 Goalw [sinl_def,sinr_def] 
         "sinl`a=sinr`b ==> a=UU & b=UU";
-by (rtac noteq_IsinlIsinr 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by (auto_tac (claset() addSDs [noteq_IsinlIsinr], simpset()));
 qed "noteq_sinlsinr";
 
 Goalw [sinl_def,sinr_def] 
         "sinl`a1=sinl`a2==> a1=a2";
-by (rtac inject_Isinl 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by Auto_tac;
 qed "inject_sinl";
 
 Goalw [sinl_def,sinr_def] 
         "sinr`a1=sinr`a2==> a1=a2";
-by (rtac inject_Isinr 1);
-by (etac box_equals 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
-by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1);
+by Auto_tac;
 qed "inject_sinr";
 
+AddSDs [inject_sinl, inject_sinr];
 
 Goal "x~=UU ==> sinl`x ~= UU";
-by (etac swap 1);
+by (etac contrapos_nn 1);
 by (rtac inject_sinl 1);
-by (stac strict_sinl 1);
-by (etac notnotD 1);
+by Auto_tac;
 qed "defined_sinl";
+Addsimps [defined_sinl];
 
 Goal "x~=UU ==> sinr`x ~= UU";
-by (etac swap 1);
+by (etac contrapos_nn 1);
 by (rtac inject_sinr 1);
-by (stac strict_sinr 1);
-by (etac notnotD 1);
+by Auto_tac;
 qed "defined_sinr";
+Addsimps [defined_sinr];
 
 Goalw [sinl_def,sinr_def] 
         "z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)";
@@ -415,6 +409,7 @@
 by tac;
 by (simp_tac Ssum0_ss  1);
 qed "sscase1";
+Addsimps [sscase1];
 
 
 val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
@@ -432,6 +427,7 @@
 by tac;
 by (asm_simp_tac Ssum0_ss  1);
 qed "sscase2";
+Addsimps [sscase2];
 
 Goalw [sscase_def,sinl_def,sinr_def] 
         "x~=UU==> sscase`f`g`(sinr`x) = g`x";
@@ -445,6 +441,7 @@
 by tac;
 by (asm_simp_tac Ssum0_ss  1);
 qed "sscase3";
+Addsimps [sscase3];
 
 
 Goalw [sinl_def,sinr_def] 
@@ -561,12 +558,9 @@
 by (atac 1);
 qed "thelub_ssum3";
 
-
 Goal "sscase`sinl`sinr`z=z";
 by (res_inst_tac [("p","z")] ssumE 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
-by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
+by Auto_tac;
 qed "sscase4";
 
 
@@ -576,6 +570,3 @@
 
 val Ssum_rews = [strict_sinl,strict_sinr,defined_sinl,defined_sinr,
                 sscase1,sscase2,sscase3];
-
-Addsimps [strict_sinl,strict_sinr,defined_sinl,defined_sinr,
-                sscase1,sscase2,sscase3];
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/Up3.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -24,6 +24,7 @@
 by (stac inst_up_pcpo 1);
 by (rtac defined_Iup 1);
 qed "defined_Iup2";
+AddIffs [defined_Iup2];
 
 (* ------------------------------------------------------------------------ *)
 (* continuity for Iup                                                       *)
@@ -49,7 +50,7 @@
 by (rtac monofun_Iup 1);
 by (rtac contlub_Iup 1);
 qed "cont_Iup";
-
+AddIffs [cont_Iup];
 
 (* ------------------------------------------------------------------------ *)
 (* continuity for Ifup                                                     *)
@@ -132,7 +133,7 @@
 (* continuous versions of lemmas for ('a)u                                  *)
 (* ------------------------------------------------------------------------ *)
 
-Goalw [up_def] "z = UU | (? x. z = up`x)";
+Goalw [up_def] "z = UU | (EX x. z = up`x)";
 by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
 by (stac inst_up_pcpo 1);
 by (rtac Exh_Up 1);
@@ -140,14 +141,11 @@
 
 Goalw [up_def] "up`x=up`y ==> x=y";
 by (rtac inject_Iup 1);
-by (etac box_equals 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
+by Auto_tac;
 qed "inject_up";
 
 Goalw [up_def] " up`x ~= UU";
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
-by (rtac defined_Iup2 1);
+by Auto_tac;
 qed "defined_up";
 
 val prems = Goalw [up_def] 
@@ -193,7 +191,7 @@
 qed "less_up4c";
 
 Goalw [up_def,fup_def] 
-"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
+"[| chain(Y); EX i x. Y(i) = up`x |] ==>\
 \      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))";
 by (stac beta_cfun 1);
 by tac;
@@ -222,16 +220,11 @@
 by (strip_tac 1);
 by (dtac spec 1);
 by (dtac spec 1);
-by (rtac swap 1);
-by (atac 1);
-by (dtac notnotD 1);
-by (etac box_equals 1);
-by (rtac refl 1);
-by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
+by (asm_full_simp_tac (Up0_ss addsimps [cont_Iup]) 1);
 qed "thelub_up2b";
 
 
-Goal "(? x. z = up`x) = (z~=UU)";
+Goal "(EX x. z = up`x) = (z~=UU)";
 by (rtac iffI 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
@@ -243,7 +236,7 @@
 qed "up_lemma2";
 
 
-Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x";
+Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> EX i x. Y(i) = up`x";
 by (rtac exE 1);
 by (rtac chain_UU_I_inverse2 1);
 by (rtac (up_lemma2 RS iffD1) 1);
@@ -254,11 +247,8 @@
 qed "thelub_up2a_rev";
 
 Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x";
-by (rtac allI 1);
-by (rtac (not_ex RS iffD1) 1);
-by (rtac contrapos 1);
-by (etac (up_lemma2 RS iffD1) 2);
-by (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1);
+by (blast_tac (claset() addSDs [chain_UU_I RS spec, 
+                                exI RS (up_lemma2 RS iffD1)]) 1);
 qed "thelub_up2b_rev";
 
 
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/domain/theorems.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -43,10 +43,9 @@
                                 cut_facts_tac prems 1,
                                 fast_tac HOL_cs 1]);
 
-val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
-                                rtac rev_contrapos 1,
-                                etac (antisym_less_inverse RS conjunct1) 1,
-                                resolve_tac prems 1]);
+val dist_eqI = prove_goal Porder.thy "!!x::'a::po. ~ x << y ==> x ~= y" 
+             (fn prems => [
+               (blast_tac (claset() addDs [antisym_less_inverse]) 1)]);
 (*
 infixr 0 y;
 val b = 0;
diff -r 10e2d29a77de -r 5eb935d6cc69 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOLCF/ex/Stream.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -24,7 +24,7 @@
 
 Goal "a && s = UU = (a = UU)";
 by Safe_tac;
-by (etac contrapos2 1);
+by (etac contrapos_pp 1);
 by (safe_tac (claset() addSIs stream.con_rews));
 qed "scons_eq_UU";