--- a/src/HOL/Bali/TypeSafe.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Thu Jan 05 22:29:55 2006 +0100
@@ -169,7 +169,7 @@
lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
apply (unfold fits_def)
apply clarify
-apply (erule swap, simp (no_asm_use))
+apply (erule contrapos_np, simp (no_asm_use))
apply (drule conf_RefTD)
apply auto
done
--- a/src/HOL/Hyperreal/NthRoot.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy Thu Jan 05 22:29:55 2006 +0100
@@ -107,7 +107,7 @@
lemma not_isUb_less_ex:
"~ isUb (UNIV::real set) S u ==> \<exists>x \<in> S. u < x"
-apply (rule ccontr, erule swap)
+apply (rule ccontr, erule contrapos_np)
apply (rule setleI [THEN isUbI])
apply (auto simp add: linorder_not_less [symmetric])
done
--- a/src/HOL/Hyperreal/Poly.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Hyperreal/Poly.thy Thu Jan 05 22:29:55 2006 +0100
@@ -497,7 +497,7 @@
lemma poly_roots_finite: "(poly p \<noteq> poly []) =
(\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))"
apply safe
-apply (erule swap, rule ext)
+apply (erule contrapos_np, rule ext)
apply (rule ccontr)
apply (clarify dest!: poly_roots_finite_lemma)
apply (clarify dest!: real_finite_lemma)
@@ -717,7 +717,7 @@
apply simp
apply (induct_tac "n")
apply (simp del: pmult_Cons pexp_Suc)
-apply (erule_tac Pa = "poly q a = 0" in swap)
+apply (erule_tac Q = "poly q a = 0" in contrapos_np)
apply (simp add: poly_add poly_cmult)
apply (rule pexp_Suc [THEN ssubst])
apply (rule ccontr)
@@ -857,8 +857,8 @@
apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
apply (unfold divides_def)
apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
-apply (rule swap, assumption)
-apply (rotate_tac 3, erule swap)
+apply (rule contrapos_np, assumption)
+apply (rotate_tac 3, erule contrapos_np)
apply (simp del: pmult_Cons pexp_Suc, safe)
apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
--- a/src/HOL/Hyperreal/SEQ.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Thu Jan 05 22:29:55 2006 +0100
@@ -436,7 +436,7 @@
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
apply (induct_tac "ka")
apply (auto intro: order_trans)
-apply (erule swap)
+apply (erule contrapos_np)
apply (induct_tac "k")
apply (auto intro: order_trans)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu Jan 05 22:29:55 2006 +0100
@@ -1624,7 +1624,7 @@
"[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
apply (rule ccontr)
apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
-apply (erule swap)
+apply (erule contrapos_np)
apply (simp del: minus_sin_cos_eq [symmetric])
apply (cut_tac y="-y" in cos_total, simp) apply simp
apply (erule ex1E)
--- a/src/HOL/Library/Zorn.thy Thu Jan 05 22:29:53 2006 +0100
+++ b/src/HOL/Library/Zorn.thy Thu Jan 05 22:29:55 2006 +0100
@@ -53,7 +53,7 @@
apply (unfold succ_def)
apply (rule split_if [THEN iffD2])
apply (auto simp add: super_def maxchain_def psubset_def)
- apply (rule swap, assumption)
+ apply (rule contrapos_np, assumption)
apply (rule someI2, blast+)
done