# HG changeset patch
# User wenzelm
# Date 1136496595 -3600
# Node ID 5d379fe2eb741755f93ae0520f293e3683c0fdc1
# Parent  0fde75d34f8d4401714c8e7db970bcec786c21c9
replaced swap by contrapos_np;

diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Bali/TypeSafe.thy
--- 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
diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Hyperreal/NthRoot.thy
--- 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
diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Hyperreal/Poly.thy
--- 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))))) ")
diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Hyperreal/SEQ.thy
--- 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
diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Hyperreal/Transcendental.thy
--- 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)
diff -r 0fde75d34f8d -r 5d379fe2eb74 src/HOL/Library/Zorn.thy
--- 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