# HG changeset patch
# User blanchet
# Date 1382085800 -7200
# Node ID 97a8ff4e4ac95ff4d7991359c3963f538b089cde
# Parent  97f69d44f73240d8e7d06f3627e5ce43efdee7de
killed most "no_atp", to make Sledgehammer more complete

diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -1999,35 +1999,35 @@
   assumes fin_nonempty: "finite A" "A \<noteq> {}"
 begin
 
-lemma Min_ge_iff [simp, no_atp]:
+lemma Min_ge_iff [simp]:
   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   using fin_nonempty by (fact Min.bounded_iff)
 
-lemma Max_le_iff [simp, no_atp]:
+lemma Max_le_iff [simp]:
   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   using fin_nonempty by (fact Max.bounded_iff)
 
-lemma Min_gr_iff [simp, no_atp]:
+lemma Min_gr_iff [simp]:
   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
 
-lemma Max_less_iff [simp, no_atp]:
+lemma Max_less_iff [simp]:
   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
 
-lemma Min_le_iff [no_atp]:
+lemma Min_le_iff:
   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
 
-lemma Max_ge_iff [no_atp]:
+lemma Max_ge_iff:
   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
 
-lemma Min_less_iff [no_atp]:
+lemma Min_less_iff:
   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
 
-lemma Max_gr_iff [no_atp]:
+lemma Max_gr_iff:
   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
 
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -93,12 +93,12 @@
 context complete_lattice
 begin
 
-lemma INF_foundation_dual [no_atp]:
+lemma INF_foundation_dual:
   "complete_lattice.SUPR Inf = INFI"
   by (simp add: fun_eq_iff INF_def
     complete_lattice.SUP_def [OF dual_complete_lattice])
 
-lemma SUP_foundation_dual [no_atp]:
+lemma SUP_foundation_dual:
   "complete_lattice.INFI Sup = SUPR"
   by (simp add: fun_eq_iff SUP_def
     complete_lattice.INF_def [OF dual_complete_lattice])
@@ -306,7 +306,7 @@
   show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
 qed
 
-lemma Inf_top_conv [simp, no_atp]:
+lemma Inf_top_conv [simp]:
   "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
   "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
 proof -
@@ -333,7 +333,7 @@
  "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
   by (auto simp add: INF_def)
 
-lemma Sup_bot_conv [simp, no_atp]:
+lemma Sup_bot_conv [simp]:
   "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   using dual_complete_lattice
@@ -769,7 +769,7 @@
     by (simp add: Inf_set_def image_def)
 qed
 
-lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
+lemma Inter_iff [simp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
   by (unfold Inter_eq) blast
 
 lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
@@ -814,7 +814,7 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by (fact Inf_union_distrib)
 
-lemma Inter_UNIV_conv [simp, no_atp]:
+lemma Inter_UNIV_conv [simp]:
   "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   by (fact Inf_top_conv)+
@@ -952,7 +952,7 @@
     by (simp add: Sup_set_def image_def)
 qed
 
-lemma Union_iff [simp, no_atp]:
+lemma Union_iff [simp]:
   "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   by (unfold Union_eq) blast
 
@@ -987,10 +987,10 @@
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   by (fact Sup_inter_less_eq)
 
-lemma Union_empty_conv [no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   by (fact Sup_bot_conv) (* already simp *)
 
-lemma empty_Union_conv [no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
   by (fact Sup_bot_conv) (* already simp *)
 
 lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
@@ -1044,7 +1044,7 @@
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
 *} -- {* to avoid eta-contraction of body *}
 
-lemma UNION_eq [no_atp]:
+lemma UNION_eq:
   "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   by (auto simp add: SUP_def)
 
@@ -1088,13 +1088,13 @@
 lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (fact SUP_least)
 
-lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   by blast
 
 lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
-lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
+lemma UN_empty: "(\<Union>x\<in>{}. B x) = {}"
   by (fact SUP_empty)
 
 lemma UN_empty2: "(\<Union>x\<in>A. {}) = {}"
@@ -1126,7 +1126,7 @@
   "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   by (fact SUP_bot_conv)+ (* already simp *)
 
-lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   by blast
 
 lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
@@ -1248,7 +1248,7 @@
   "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
   by auto
 
-lemma UN_ball_bex_simps [simp, no_atp]:
+lemma UN_ball_bex_simps [simp]:
   "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
   "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
   "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Fields.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -152,7 +152,7 @@
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
   by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
-lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
+lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
   by (simp add: divide_inverse)
 
 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -252,7 +252,7 @@
    ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
 by (simp add: division_ring_inverse_add mult_ac)
 
-lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
 proof -
   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
@@ -263,7 +263,7 @@
     finally show ?thesis by (simp add: divide_inverse)
 qed
 
-lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_right [simp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
 by (simp add: mult_commute [of _ c])
 
@@ -275,7 +275,7 @@
   fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
   many proofs seem to need them.*}
 
-lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
 
 lemma add_frac_eq:
   assumes "y \<noteq> 0" and "z \<noteq> 0"
@@ -291,27 +291,27 @@
 
 text{*Special Cancellation Simprules for Division*}
 
-lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
+lemma nonzero_mult_divide_cancel_right [simp]:
   "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
   using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
 
-lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
+lemma nonzero_mult_divide_cancel_left [simp]:
   "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
 
-lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
+lemma nonzero_divide_mult_cancel_right [simp]:
   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
 
-lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
+lemma nonzero_divide_mult_cancel_left [simp]:
   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
 
-lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
 using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
 
-lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
 
@@ -383,18 +383,18 @@
 apply simp_all
 done
 
-lemma divide_divide_eq_right [simp, no_atp]:
+lemma divide_divide_eq_right [simp]:
   "a / (b / c) = (a * c) / b"
   by (simp add: divide_inverse mult_ac)
 
-lemma divide_divide_eq_left [simp, no_atp]:
+lemma divide_divide_eq_left [simp]:
   "(a / b) / c = a / (b * c)"
   by (simp add: divide_inverse mult_assoc)
 
 
 text {*Special Cancellation Simprules for Division*}
 
-lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
+lemma mult_divide_mult_cancel_left_if [simp]:
   shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
   by (simp add: mult_divide_mult_cancel_left)
 
@@ -405,7 +405,7 @@
   "- (a / b) = a / - b"
   by (simp add: divide_inverse)
 
-lemma divide_minus_right [simp, no_atp]:
+lemma divide_minus_right [simp]:
   "a / - b = - (a / b)"
   by (simp add: divide_inverse)
 
@@ -427,29 +427,29 @@
   "inverse x = 1 \<longleftrightarrow> x = 1"
   by (insert inverse_eq_iff_eq [of x 1], simp) 
 
-lemma divide_eq_0_iff [simp, no_atp]:
+lemma divide_eq_0_iff [simp]:
   "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   by (simp add: divide_inverse)
 
-lemma divide_cancel_right [simp, no_atp]:
+lemma divide_cancel_right [simp]:
   "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
   apply (cases "c=0", simp)
   apply (simp add: divide_inverse)
   done
 
-lemma divide_cancel_left [simp, no_atp]:
+lemma divide_cancel_left [simp]:
   "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 
   apply (cases "c=0", simp)
   apply (simp add: divide_inverse)
   done
 
-lemma divide_eq_1_iff [simp, no_atp]:
+lemma divide_eq_1_iff [simp]:
   "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   apply (cases "b=0", simp)
   apply (simp add: right_inverse_eq)
   done
 
-lemma one_eq_divide_iff [simp, no_atp]:
+lemma one_eq_divide_iff [simp]:
   "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   by (simp add: eq_commute [of 1])
 
@@ -559,7 +559,7 @@
 done
 
 text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,no_atp]:
+lemma inverse_less_iff_less [simp]:
   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
 
@@ -567,7 +567,7 @@
   "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
   by (force simp add: le_less less_imp_inverse_less)
 
-lemma inverse_le_iff_le [simp,no_atp]:
+lemma inverse_le_iff_le [simp]:
   "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
 
@@ -601,7 +601,7 @@
 apply (simp add: nonzero_inverse_minus_eq) 
 done
 
-lemma inverse_less_iff_less_neg [simp,no_atp]:
+lemma inverse_less_iff_less_neg [simp]:
   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
 apply (insert inverse_less_iff_less [of "-b" "-a"])
 apply (simp del: inverse_less_iff_less 
@@ -612,7 +612,7 @@
   "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
   by (force simp add: le_less less_imp_inverse_less_neg)
 
-lemma inverse_le_iff_le_neg [simp,no_atp]:
+lemma inverse_le_iff_le_neg [simp]:
   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
@@ -713,11 +713,9 @@
 sign_simps} to @{text field_simps} because the former can lead to case
 explosions. *}
 
-lemmas sign_simps [no_atp] = algebra_simps
-  zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
 
-lemmas (in -) sign_simps [no_atp] = algebra_simps
-  zero_less_mult_iff mult_less_0_iff
+lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
 
 (* Only works once linear arithmetic is installed:
 text{*An example:*}
@@ -998,13 +996,13 @@
 
 text{*Simplify expressions equated with 1*}
 
-lemma zero_eq_1_divide_iff [simp,no_atp]:
+lemma zero_eq_1_divide_iff [simp]:
      "(0 = 1/a) = (a = 0)"
 apply (cases "a=0", simp)
 apply (auto simp add: nonzero_eq_divide_eq)
 done
 
-lemma one_divide_eq_0_iff [simp,no_atp]:
+lemma one_divide_eq_0_iff [simp]:
      "(1/a = 0) = (a = 0)"
 apply (cases "a=0", simp)
 apply (insert zero_neq_one [THEN not_sym])
@@ -1013,19 +1011,19 @@
 
 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
 
-lemma zero_le_divide_1_iff [simp, no_atp]:
+lemma zero_le_divide_1_iff [simp]:
   "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
   by (simp add: zero_le_divide_iff)
 
-lemma zero_less_divide_1_iff [simp, no_atp]:
+lemma zero_less_divide_1_iff [simp]:
   "0 < 1 / a \<longleftrightarrow> 0 < a"
   by (simp add: zero_less_divide_iff)
 
-lemma divide_le_0_1_iff [simp, no_atp]:
+lemma divide_le_0_1_iff [simp]:
   "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
   by (simp add: divide_le_0_iff)
 
-lemma divide_less_0_1_iff [simp, no_atp]:
+lemma divide_less_0_1_iff [simp]:
   "1 / a < 0 \<longleftrightarrow> a < 0"
   by (simp add: divide_less_0_iff)
 
@@ -1080,62 +1078,62 @@
 
 text{*Simplify quotients that are compared with the value 1.*}
 
-lemma le_divide_eq_1 [no_atp]:
+lemma le_divide_eq_1:
   "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
 by (auto simp add: le_divide_eq)
 
-lemma divide_le_eq_1 [no_atp]:
+lemma divide_le_eq_1:
   "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
 by (auto simp add: divide_le_eq)
 
-lemma less_divide_eq_1 [no_atp]:
+lemma less_divide_eq_1:
   "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
 by (auto simp add: less_divide_eq)
 
-lemma divide_less_eq_1 [no_atp]:
+lemma divide_less_eq_1:
   "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
 by (auto simp add: divide_less_eq)
 
 
 text {*Conditional Simplification Rules: No Case Splits*}
 
-lemma le_divide_eq_1_pos [simp,no_atp]:
+lemma le_divide_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
 by (auto simp add: le_divide_eq)
 
-lemma le_divide_eq_1_neg [simp,no_atp]:
+lemma le_divide_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
 by (auto simp add: le_divide_eq)
 
-lemma divide_le_eq_1_pos [simp,no_atp]:
+lemma divide_le_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
 by (auto simp add: divide_le_eq)
 
-lemma divide_le_eq_1_neg [simp,no_atp]:
+lemma divide_le_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
 by (auto simp add: divide_le_eq)
 
-lemma less_divide_eq_1_pos [simp,no_atp]:
+lemma less_divide_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
 by (auto simp add: less_divide_eq)
 
-lemma less_divide_eq_1_neg [simp,no_atp]:
+lemma less_divide_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
 by (auto simp add: less_divide_eq)
 
-lemma divide_less_eq_1_pos [simp,no_atp]:
+lemma divide_less_eq_1_pos [simp]:
   "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
 by (auto simp add: divide_less_eq)
 
-lemma divide_less_eq_1_neg [simp,no_atp]:
+lemma divide_less_eq_1_neg [simp]:
   "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
 by (auto simp add: divide_less_eq)
 
-lemma eq_divide_eq_1 [simp,no_atp]:
+lemma eq_divide_eq_1 [simp]:
   "(1 = b/a) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: eq_divide_eq)
 
-lemma divide_eq_eq_1 [simp,no_atp]:
+lemma divide_eq_eq_1 [simp]:
   "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
 
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -1620,8 +1620,7 @@
   show False by simp (blast dest: Suc_neq_Zero surjD)
 qed
 
-(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
-lemma infinite_UNIV_char_0 [no_atp]:
+lemma infinite_UNIV_char_0:
   "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
 proof
   assume "finite (UNIV :: 'a set)"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -775,7 +775,7 @@
 
 subsection {* Cantor's Paradox *}
 
-lemma Cantors_paradox [no_atp]:
+lemma Cantors_paradox:
   "\<not>(\<exists>f. f ` A = Pow A)"
 proof clarify
   fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -1341,7 +1341,7 @@
 
 subsection {* Tools setup *}
 
-lemma add_mono_thms_linordered_semiring [no_atp]:
+lemma add_mono_thms_linordered_semiring:
   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
@@ -1349,7 +1349,7 @@
     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
 by (rule add_mono, clarify+)+
 
-lemma add_mono_thms_linordered_field [no_atp]:
+lemma add_mono_thms_linordered_field:
   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Int.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -450,7 +450,7 @@
       It is proved here because attribute @{text arith_split} is not available
       in theory @{text Rings}.
       But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split,no_atp]:
+lemma abs_split [arith_split, no_atp]:
      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
@@ -1158,32 +1158,32 @@
 
 text{*To Simplify Inequalities Where One Side is the Constant 1*}
 
-lemma less_minus_iff_1 [simp,no_atp]:
+lemma less_minus_iff_1 [simp]:
   fixes b::"'b::linordered_idom"
   shows "(1 < - b) = (b < -1)"
 by auto
 
-lemma le_minus_iff_1 [simp,no_atp]:
+lemma le_minus_iff_1 [simp]:
   fixes b::"'b::linordered_idom"
   shows "(1 \<le> - b) = (b \<le> -1)"
 by auto
 
-lemma equation_minus_iff_1 [simp,no_atp]:
+lemma equation_minus_iff_1 [simp]:
   fixes b::"'b::ring_1"
   shows "(1 = - b) = (b = -1)"
 by (subst equation_minus_iff, auto)
 
-lemma minus_less_iff_1 [simp,no_atp]:
+lemma minus_less_iff_1 [simp]:
   fixes a::"'b::linordered_idom"
   shows "(- a < 1) = (-1 < a)"
 by auto
 
-lemma minus_le_iff_1 [simp,no_atp]:
+lemma minus_le_iff_1 [simp]:
   fixes a::"'b::linordered_idom"
   shows "(- a \<le> 1) = (-1 \<le> a)"
 by auto
 
-lemma minus_equation_iff_1 [simp,no_atp]:
+lemma minus_equation_iff_1 [simp]:
   fixes a::"'b::ring_1"
   shows "(- a = 1) = (a = -1)"
 by (subst minus_equation_iff, auto)
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/List.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -902,7 +902,7 @@
 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
 by (induct xs) auto
 
-lemma append_eq_append_conv [simp, no_atp]:
+lemma append_eq_append_conv [simp]:
  "length xs = length ys \<or> length us = length vs
  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
 apply (induct xs arbitrary: ys)
@@ -934,7 +934,7 @@
 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
 using append_same_eq [of "[]"] by auto
 
-lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
 by (induct xs) auto
 
 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
@@ -1178,7 +1178,7 @@
 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
 by (cases xs) auto
 
-lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
+lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
 apply (induct xs arbitrary: ys, force)
 apply (case_tac ys, simp, force)
 done
@@ -5084,10 +5084,10 @@
   for A :: "'a set"
 where
     Nil [intro!, simp]: "[]: lists A"
-  | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
-inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
+  | Cons [intro!, simp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+
+inductive_cases listsE [elim!]: "x#l : lists A"
+inductive_cases listspE [elim!]: "listsp A (x # l)"
 
 inductive_simps listsp_simps[code]:
   "listsp A []"
@@ -5129,15 +5129,15 @@
 
 lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
 
-lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
 by (rule in_listsp_conv_set [THEN iffD1])
 
-lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
-
-lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemmas in_listsD [dest!] = in_listspD [to_set]
+
+lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
 by (rule in_listsp_conv_set [THEN iffD2])
 
-lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
+lemmas in_listsI [intro!] = in_listspI [to_set]
 
 lemma lists_eq_set: "lists A = {xs. set xs <= A}"
 by auto
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Nat.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -327,7 +327,7 @@
    apply auto
   done
 
-lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
+lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
   apply (rule trans)
   apply (rule_tac [2] mult_eq_1_iff, fastforce)
   done
@@ -491,7 +491,7 @@
 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   by (simp add: less_Suc_eq)
 
-lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
   unfolding One_nat_def by (rule less_Suc0)
 
 lemma Suc_mono: "m < n ==> Suc m < Suc n"
@@ -659,7 +659,7 @@
 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
 by (fast intro: not0_implies_Suc)
 
-lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
 using neq0_conv by blast
 
 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
@@ -1396,10 +1396,10 @@
 
 text{*Special cases where either operand is zero*}
 
-lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
 
-lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
 end
@@ -1432,7 +1432,7 @@
 
 text{*Special cases where either operand is zero*}
 
-lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -998,7 +998,7 @@
     (!!x y. x > y ==> f x > f y) ==> f a > c"
 by (subgoal_tac "f a > f b", force, force)
 
-lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
+lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
 
 (* 
   Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Power.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -530,7 +530,7 @@
   "abs ((-a) ^ n) = abs (a ^ n)"
   by (simp add: power_abs)
 
-lemma zero_less_power_abs_iff [simp, no_atp]:
+lemma zero_less_power_abs_iff [simp]:
   "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
 proof (induct n)
   case 0 show ?case by simp
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -75,10 +75,10 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
-lemma UNIV_unit [no_atp]:
+lemma UNIV_unit:
   "UNIV = {()}" by auto
 
 instantiation unit :: default
@@ -586,10 +586,10 @@
    to quite time-consuming computations (in particular for nested tuples) *)
 setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
 
-lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   by (rule ext) fast
 
 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Record.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -399,7 +399,7 @@
 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   by simp
 
-lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   by simp
 
 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Relation.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -478,7 +478,7 @@
 lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
   by (simp add: Id_on_def)
 
-lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
+lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A"
   by (rule Id_on_eqI) (rule refl)
 
 lemma Id_onE [elim!]:
@@ -939,8 +939,6 @@
 where
   "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
 
-declare Image_def [no_atp]
-
 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   by (simp add: Image_def)
 
@@ -950,7 +948,7 @@
 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   by (rule Image_iff [THEN trans]) simp
 
-lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
   by (unfold Image_def) blast
 
 lemma ImageE [elim!]:
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Rings.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -127,7 +127,7 @@
   then show ?thesis ..
 qed
 
-lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
+lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
 by (auto intro: dvd_refl elim!: dvdE)
 
 lemma dvd_0_right [iff]: "a dvd 0"
@@ -233,8 +233,8 @@
 by (rule minus_unique) (simp add: distrib_left [symmetric]) 
 
 text{*Extract signs from products*}
-lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
 
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
 by simp
@@ -248,7 +248,7 @@
 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
 by (simp add: distrib_right diff_minus)
 
-lemmas ring_distribs[no_atp] =
+lemmas ring_distribs =
   distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 lemma eq_add_iff1:
@@ -261,7 +261,7 @@
 
 end
 
-lemmas ring_distribs[no_atp] =
+lemmas ring_distribs =
   distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
@@ -336,7 +336,7 @@
 qed
 
 text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp, no_atp]:
+lemma mult_cancel_right [simp]:
   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(a * c = b * c) = ((a - b) * c = 0)"
@@ -344,7 +344,7 @@
   thus ?thesis by (simp add: disj_commute)
 qed
 
-lemma mult_cancel_left [simp, no_atp]:
+lemma mult_cancel_left [simp]:
   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(c * a = c * b) = (c * (a - b) = 0)"
@@ -1048,7 +1048,7 @@
 
 text {* Simprules for comparisons where common factors can be cancelled. *}
 
-lemmas mult_compare_simps[no_atp] =
+lemmas mult_compare_simps =
     mult_le_cancel_right mult_le_cancel_left
     mult_le_cancel_right1 mult_le_cancel_right2
     mult_le_cancel_left1 mult_le_cancel_left2
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Set.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -87,7 +87,7 @@
   then show ?thesis by simp
 qed
 
-lemma set_eq_iff [no_atp]:
+lemma set_eq_iff:
   "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
   by (auto intro:set_eqI)
 
@@ -495,7 +495,7 @@
   by (simp add: less_eq_set_def le_fun_def)
   -- {* Rule in Modus Ponens style. *}
 
-lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   -- {* The same, with reversed premises for use with @{text erule} --
       cf @{text rev_mp}. *}
   by (rule subsetD)
@@ -504,13 +504,13 @@
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
 
-lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   by (auto simp add: less_eq_set_def le_fun_def)
 
-lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
-
-lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+
+lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
 lemma subset_refl: "A \<subseteq> A"
@@ -845,11 +845,11 @@
 
 subsubsection {* Singletons, using insert *}
 
-lemma singletonI [intro!,no_atp]: "a : {a}"
+lemma singletonI [intro!]: "a : {a}"
     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   by (rule insertI1)
 
-lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
+lemma singletonD [dest!]: "b : {a} ==> b = a"
   by blast
 
 lemmas singletonE = singletonD [elim_format]
@@ -860,11 +860,11 @@
 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   by blast
 
-lemma singleton_insert_inj_eq [iff,no_atp]:
+lemma singleton_insert_inj_eq [iff]:
      "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   by blast
 
-lemma singleton_insert_inj_eq' [iff,no_atp]:
+lemma singleton_insert_inj_eq' [iff]:
      "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   by blast
 
@@ -898,7 +898,7 @@
 *}
 
 definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
-  image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
+  image_def: "f ` A = {y. EX x:A. y = f(x)}"
 
 abbreviation
   range :: "('a => 'b) => 'b set" where -- "of function"
@@ -930,7 +930,7 @@
 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   by blast
 
-lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   -- {* This rewrite rule would confuse users if made default. *}
   by blast
 
@@ -1009,10 +1009,10 @@
 
 subsubsection {* The ``proper subset'' relation *}
 
-lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
+lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   by (unfold less_le) blast
 
-lemma psubsetE [elim!,no_atp]:
+lemma psubsetE [elim!]:
     "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   by (unfold less_le) blast
 
@@ -1184,12 +1184,12 @@
 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   by blast
 
-lemma insert_disjoint [simp,no_atp]:
+lemma insert_disjoint [simp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
   by auto
 
-lemma disjoint_insert [simp,no_atp]:
+lemma disjoint_insert [simp]:
  "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   by auto
@@ -1221,7 +1221,7 @@
 by blast
 
 
-lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
+lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
   -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
       with its implicit quantifier and conjunction.  Also image enjoys better
       equational properties than does the RHS. *}
@@ -1244,7 +1244,7 @@
 
 text {* \medskip @{text range}. *}
 
-lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
+lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
   by auto
 
 lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
@@ -1301,10 +1301,10 @@
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   by (fact inf_sup_distrib2)
 
-lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   by (fact inf_eq_top_iff) (* already simp *)
 
-lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   by (fact le_inf_iff)
 
 lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1395,7 +1395,7 @@
 lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   by (fact sup_eq_bot_iff) (* FIXME: already simp *)
 
-lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   by (fact le_sup_iff)
 
 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1467,7 +1467,7 @@
 lemma Diff_eq: "A - B = A \<inter> (-B)"
   by blast
 
-lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
+lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
   by blast
 
 lemma Diff_cancel [simp]: "A - A = {}"
@@ -1488,7 +1488,7 @@
 lemma Diff_UNIV [simp]: "A - UNIV = {}"
   by blast
 
-lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
+lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
   by blast
 
 lemma Diff_insert: "A - insert a B = A - B - {a}"
@@ -1568,7 +1568,7 @@
 lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   by (auto intro: bool_contrapos)
 
-lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
+lemma UNIV_bool: "UNIV = {False, True}"
   by (auto intro: bool_induct)
 
 text {* \medskip @{text Pow} *}
@@ -1597,7 +1597,7 @@
 lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
   by blast
 
-lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
   by blast
 
 lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
@@ -1754,7 +1754,7 @@
   -- {* monotonicity *}
   by blast
 
-lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
 by (blast intro: sym)
 
 lemma image_vimage_subset: "f ` (f -` A) <= A"
diff -r 97f69d44f732 -r 97a8ff4e4ac9 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Set_Interval.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -180,19 +180,19 @@
 context ord
 begin
 
-lemma greaterThanLessThan_iff [simp,no_atp]:
+lemma greaterThanLessThan_iff [simp]:
   "(i : {l<..<u}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
-lemma atLeastLessThan_iff [simp,no_atp]:
+lemma atLeastLessThan_iff [simp]:
   "(i : {l..<u}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
-lemma greaterThanAtMost_iff [simp,no_atp]:
+lemma greaterThanAtMost_iff [simp]:
   "(i : {l<..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
-lemma atLeastAtMost_iff [simp,no_atp]:
+lemma atLeastAtMost_iff [simp]:
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
@@ -1196,7 +1196,7 @@
 
 subsubsection {* Some Subset Conditions *}
 
-lemma ivl_subset [simp,no_atp]:
+lemma ivl_subset [simp]:
  "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
 apply(auto simp:linorder_not_le)
 apply(rule ccontr)