now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
authorblanchet
Thu Mar 18 12:58:52 2010 +0100 (2010-03-18)
changeset 3582846cfc4b8112e
parent 35827 f552152d7747
child 35829 c5f54c04a1aa
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattice.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Fields.thy
src/HOL/Finite_Set.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/IsaMakefile
src/HOL/Library/Lattice_Algebras.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Rings.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/res_blacklist.ML
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -1534,12 +1534,12 @@
     1.4    from assms show ?thesis by (simp add: Max_def fold1_belowI)
     1.5  qed
     1.6  
     1.7 -lemma Min_ge_iff [simp, noatp]:
     1.8 +lemma Min_ge_iff [simp, no_atp]:
     1.9    assumes "finite A" and "A \<noteq> {}"
    1.10    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
    1.11    using assms by (simp add: Min_def min_max.below_fold1_iff)
    1.12  
    1.13 -lemma Max_le_iff [simp, noatp]:
    1.14 +lemma Max_le_iff [simp, no_atp]:
    1.15    assumes "finite A" and "A \<noteq> {}"
    1.16    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
    1.17  proof -
    1.18 @@ -1548,12 +1548,12 @@
    1.19    from assms show ?thesis by (simp add: Max_def below_fold1_iff)
    1.20  qed
    1.21  
    1.22 -lemma Min_gr_iff [simp, noatp]:
    1.23 +lemma Min_gr_iff [simp, no_atp]:
    1.24    assumes "finite A" and "A \<noteq> {}"
    1.25    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
    1.26    using assms by (simp add: Min_def strict_below_fold1_iff)
    1.27  
    1.28 -lemma Max_less_iff [simp, noatp]:
    1.29 +lemma Max_less_iff [simp, no_atp]:
    1.30    assumes "finite A" and "A \<noteq> {}"
    1.31    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
    1.32  proof -
    1.33 @@ -1563,12 +1563,12 @@
    1.34      by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
    1.35  qed
    1.36  
    1.37 -lemma Min_le_iff [noatp]:
    1.38 +lemma Min_le_iff [no_atp]:
    1.39    assumes "finite A" and "A \<noteq> {}"
    1.40    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
    1.41    using assms by (simp add: Min_def fold1_below_iff)
    1.42  
    1.43 -lemma Max_ge_iff [noatp]:
    1.44 +lemma Max_ge_iff [no_atp]:
    1.45    assumes "finite A" and "A \<noteq> {}"
    1.46    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
    1.47  proof -
    1.48 @@ -1578,12 +1578,12 @@
    1.49      by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
    1.50  qed
    1.51  
    1.52 -lemma Min_less_iff [noatp]:
    1.53 +lemma Min_less_iff [no_atp]:
    1.54    assumes "finite A" and "A \<noteq> {}"
    1.55    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
    1.56    using assms by (simp add: Min_def fold1_strict_below_iff)
    1.57  
    1.58 -lemma Max_gr_iff [noatp]:
    1.59 +lemma Max_gr_iff [no_atp]:
    1.60    assumes "finite A" and "A \<noteq> {}"
    1.61    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
    1.62  proof -
     2.1 --- a/src/HOL/Complete_Lattice.thy	Wed Mar 17 19:37:44 2010 +0100
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Mar 18 12:58:52 2010 +0100
     2.3 @@ -231,7 +231,7 @@
     2.4      by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
     2.5  qed
     2.6  
     2.7 -lemma Union_iff [simp, noatp]:
     2.8 +lemma Union_iff [simp, no_atp]:
     2.9    "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
    2.10    by (unfold Union_eq) blast
    2.11  
    2.12 @@ -269,10 +269,10 @@
    2.13  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
    2.14    by blast
    2.15  
    2.16 -lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    2.17 +lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    2.18    by blast
    2.19  
    2.20 -lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    2.21 +lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    2.22    by blast
    2.23  
    2.24  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
    2.25 @@ -332,7 +332,7 @@
    2.26    "\<Union>S = (\<Union>x\<in>S. x)"
    2.27    by (simp add: UNION_eq_Union_image image_def)
    2.28  
    2.29 -lemma UNION_def [noatp]:
    2.30 +lemma UNION_def [no_atp]:
    2.31    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
    2.32    by (auto simp add: UNION_eq_Union_image Union_eq)
    2.33    
    2.34 @@ -368,13 +368,13 @@
    2.35  lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
    2.36    by (iprover intro: subsetI elim: UN_E dest: subsetD)
    2.37  
    2.38 -lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    2.39 +lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    2.40    by blast
    2.41  
    2.42  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
    2.43    by blast
    2.44  
    2.45 -lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
    2.46 +lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
    2.47    by blast
    2.48  
    2.49  lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
    2.50 @@ -412,7 +412,7 @@
    2.51    "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
    2.52  by blast+
    2.53  
    2.54 -lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
    2.55 +lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
    2.56    by blast
    2.57  
    2.58  lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
    2.59 @@ -467,7 +467,7 @@
    2.60      by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
    2.61  qed
    2.62  
    2.63 -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
    2.64 +lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
    2.65    by (unfold Inter_eq) blast
    2.66  
    2.67  lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
    2.68 @@ -515,7 +515,7 @@
    2.69  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    2.70    by blast
    2.71  
    2.72 -lemma Inter_UNIV_conv [simp,noatp]:
    2.73 +lemma Inter_UNIV_conv [simp,no_atp]:
    2.74    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
    2.75    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
    2.76    by blast+
    2.77 @@ -724,7 +724,7 @@
    2.78    "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
    2.79    by auto
    2.80  
    2.81 -lemma ball_simps [simp,noatp]:
    2.82 +lemma ball_simps [simp,no_atp]:
    2.83    "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
    2.84    "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
    2.85    "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
    2.86 @@ -739,7 +739,7 @@
    2.87    "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
    2.88    by auto
    2.89  
    2.90 -lemma bex_simps [simp,noatp]:
    2.91 +lemma bex_simps [simp,no_atp]:
    2.92    "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
    2.93    "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
    2.94    "!!P. (EX x:{}. P x) = False"
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 17 19:37:44 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Mar 18 12:58:52 2010 +0100
     3.3 @@ -19,9 +19,9 @@
     3.4  context linorder
     3.5  begin
     3.6  
     3.7 -lemma less_not_permute[noatp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
     3.8 +lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
     3.9  
    3.10 -lemma gather_simps[noatp]: 
    3.11 +lemma gather_simps[no_atp]: 
    3.12    shows 
    3.13    "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
    3.14    and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
    3.15 @@ -29,61 +29,61 @@
    3.16    and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"  by auto
    3.17  
    3.18  lemma 
    3.19 -  gather_start[noatp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
    3.20 +  gather_start[no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
    3.21    by simp
    3.22  
    3.23  text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
    3.24 -lemma minf_lt[noatp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
    3.25 -lemma minf_gt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
    3.26 +lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
    3.27 +lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
    3.28    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    3.29  
    3.30 -lemma minf_le[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
    3.31 -lemma minf_ge[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
    3.32 +lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
    3.33 +lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
    3.34    by (auto simp add: less_le not_less not_le)
    3.35 -lemma minf_eq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    3.36 -lemma minf_neq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    3.37 -lemma minf_P[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    3.38 +lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    3.39 +lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    3.40 +lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    3.41  
    3.42  text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
    3.43 -lemma pinf_gt[noatp]:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
    3.44 -lemma pinf_lt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
    3.45 +lemma pinf_gt[no_atp]:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
    3.46 +lemma pinf_lt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
    3.47    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    3.48  
    3.49 -lemma pinf_ge[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
    3.50 -lemma pinf_le[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
    3.51 +lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
    3.52 +lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
    3.53    by (auto simp add: less_le not_less not_le)
    3.54 -lemma pinf_eq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    3.55 -lemma pinf_neq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    3.56 -lemma pinf_P[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    3.57 +lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    3.58 +lemma pinf_neq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    3.59 +lemma pinf_P[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    3.60  
    3.61 -lemma nmi_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.62 -lemma nmi_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    3.63 +lemma nmi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.64 +lemma nmi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    3.65    by (auto simp add: le_less)
    3.66 -lemma  nmi_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.67 -lemma  nmi_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.68 -lemma  nmi_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.69 -lemma  nmi_neq[noatp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.70 -lemma  nmi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.71 -lemma  nmi_conj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    3.72 +lemma  nmi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.73 +lemma  nmi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.74 +lemma  nmi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.75 +lemma  nmi_neq[no_atp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.76 +lemma  nmi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.77 +lemma  nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    3.78    \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
    3.79    \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.80 -lemma  nmi_disj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    3.81 +lemma  nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    3.82    \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
    3.83    \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    3.84  
    3.85 -lemma  npi_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x < t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
    3.86 -lemma  npi_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.87 -lemma  npi_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.88 -lemma  npi_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.89 -lemma  npi_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.90 -lemma  npi_neq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u )" by auto
    3.91 -lemma  npi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.92 -lemma  npi_conj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
    3.93 +lemma  npi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x < t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
    3.94 +lemma  npi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.95 +lemma  npi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.96 +lemma  npi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.97 +lemma  npi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    3.98 +lemma  npi_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u )" by auto
    3.99 +lemma  npi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
   3.100 +lemma  npi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   3.101    \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
   3.102 -lemma  npi_disj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   3.103 +lemma  npi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   3.104    \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
   3.105  
   3.106 -lemma lin_dense_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
   3.107 +lemma lin_dense_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
   3.108  proof(clarsimp)
   3.109    fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
   3.110      and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
   3.111 @@ -96,7 +96,7 @@
   3.112    thus "y < t" using tny by (simp add: less_le)
   3.113  qed
   3.114  
   3.115 -lemma lin_dense_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
   3.116 +lemma lin_dense_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
   3.117  proof(clarsimp)
   3.118    fix x l u y
   3.119    assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   3.120 @@ -109,7 +109,7 @@
   3.121    thus "t < y" using tny by (simp add:less_le)
   3.122  qed
   3.123  
   3.124 -lemma lin_dense_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
   3.125 +lemma lin_dense_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
   3.126  proof(clarsimp)
   3.127    fix x l u y
   3.128    assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   3.129 @@ -122,7 +122,7 @@
   3.130    hence "\<not> t < y"  by auto thus "y \<le> t" by (simp add: not_less)
   3.131  qed
   3.132  
   3.133 -lemma lin_dense_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
   3.134 +lemma lin_dense_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
   3.135  proof(clarsimp)
   3.136    fix x l u y
   3.137    assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   3.138 @@ -134,11 +134,11 @@
   3.139      with tU noU have "False" by auto}
   3.140    hence "\<not> y<t"  by auto thus "t \<le> y" by (simp add: not_less)
   3.141  qed
   3.142 -lemma lin_dense_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"  by auto
   3.143 -lemma lin_dense_neq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"  by auto
   3.144 -lemma lin_dense_P[noatp]: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"  by auto
   3.145 +lemma lin_dense_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"  by auto
   3.146 +lemma lin_dense_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"  by auto
   3.147 +lemma lin_dense_P[no_atp]: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"  by auto
   3.148  
   3.149 -lemma lin_dense_conj[noatp]:
   3.150 +lemma lin_dense_conj[no_atp]:
   3.151    "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
   3.152    \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   3.153    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
   3.154 @@ -146,7 +146,7 @@
   3.155    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
   3.156    \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   3.157    by blast
   3.158 -lemma lin_dense_disj[noatp]:
   3.159 +lemma lin_dense_disj[no_atp]:
   3.160    "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
   3.161    \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   3.162    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
   3.163 @@ -155,11 +155,11 @@
   3.164    \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
   3.165    by blast
   3.166  
   3.167 -lemma npmibnd[noatp]: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   3.168 +lemma npmibnd[no_atp]: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   3.169    \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
   3.170  by auto
   3.171  
   3.172 -lemma finite_set_intervals[noatp]:
   3.173 +lemma finite_set_intervals[no_atp]:
   3.174    assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   3.175    and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   3.176    shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
   3.177 @@ -191,7 +191,7 @@
   3.178    from ainS binS noy ax xb px show ?thesis by blast
   3.179  qed
   3.180  
   3.181 -lemma finite_set_intervals2[noatp]:
   3.182 +lemma finite_set_intervals2[no_atp]:
   3.183    assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   3.184    and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   3.185    shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
   3.186 @@ -215,7 +215,7 @@
   3.187    "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
   3.188    by (auto dest: dense)
   3.189  
   3.190 -lemma dlo_qe_bnds[noatp]: 
   3.191 +lemma dlo_qe_bnds[no_atp]: 
   3.192    assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   3.193    shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
   3.194  proof (simp only: atomize_eq, rule iffI)
   3.195 @@ -239,7 +239,7 @@
   3.196    ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
   3.197  qed
   3.198  
   3.199 -lemma dlo_qe_noub[noatp]: 
   3.200 +lemma dlo_qe_noub[no_atp]: 
   3.201    assumes ne: "L \<noteq> {}" and fL: "finite L"
   3.202    shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
   3.203  proof(simp add: atomize_eq)
   3.204 @@ -249,7 +249,7 @@
   3.205    thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
   3.206  qed
   3.207  
   3.208 -lemma dlo_qe_nolb[noatp]: 
   3.209 +lemma dlo_qe_nolb[no_atp]: 
   3.210    assumes ne: "U \<noteq> {}" and fU: "finite U"
   3.211    shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
   3.212  proof(simp add: atomize_eq)
   3.213 @@ -259,14 +259,14 @@
   3.214    thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
   3.215  qed
   3.216  
   3.217 -lemma exists_neq[noatp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
   3.218 +lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
   3.219    using gt_ex[of t] by auto
   3.220  
   3.221 -lemmas dlo_simps[noatp] = order_refl less_irrefl not_less not_le exists_neq 
   3.222 +lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
   3.223    le_less neq_iff linear less_not_permute
   3.224  
   3.225 -lemma axiom[noatp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
   3.226 -lemma atoms[noatp]:
   3.227 +lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
   3.228 +lemma atoms[no_atp]:
   3.229    shows "TERM (less :: 'a \<Rightarrow> _)"
   3.230      and "TERM (less_eq :: 'a \<Rightarrow> _)"
   3.231      and "TERM (op = :: 'a \<Rightarrow> _)" .
   3.232 @@ -277,21 +277,21 @@
   3.233  end
   3.234  
   3.235  (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
   3.236 -lemma dnf[noatp]:
   3.237 +lemma dnf[no_atp]:
   3.238    "(P & (Q | R)) = ((P&Q) | (P&R))" 
   3.239    "((Q | R) & P) = ((Q&P) | (R&P))"
   3.240    by blast+
   3.241  
   3.242 -lemmas weak_dnf_simps[noatp] = simp_thms dnf
   3.243 +lemmas weak_dnf_simps[no_atp] = simp_thms dnf
   3.244  
   3.245 -lemma nnf_simps[noatp]:
   3.246 +lemma nnf_simps[no_atp]:
   3.247      "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   3.248      "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   3.249    by blast+
   3.250  
   3.251 -lemma ex_distrib[noatp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
   3.252 +lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
   3.253  
   3.254 -lemmas dnf_simps[noatp] = weak_dnf_simps nnf_simps ex_distrib
   3.255 +lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
   3.256  
   3.257  use "~~/src/HOL/Tools/Qelim/langford.ML"
   3.258  method_setup dlo = {*
   3.259 @@ -316,10 +316,10 @@
   3.260  locale linorder_no_ub = linorder_stupid_syntax +
   3.261    assumes gt_ex: "\<exists>y. less x y"
   3.262  begin
   3.263 -lemma ge_ex[noatp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
   3.264 +lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
   3.265  
   3.266  text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
   3.267 -lemma pinf_conj[noatp]:
   3.268 +lemma pinf_conj[no_atp]:
   3.269    assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   3.270    and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   3.271    shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   3.272 @@ -335,7 +335,7 @@
   3.273    thus ?thesis by blast
   3.274  qed
   3.275  
   3.276 -lemma pinf_disj[noatp]:
   3.277 +lemma pinf_disj[no_atp]:
   3.278    assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   3.279    and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   3.280    shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   3.281 @@ -351,7 +351,7 @@
   3.282    thus ?thesis by blast
   3.283  qed
   3.284  
   3.285 -lemma pinf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   3.286 +lemma pinf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   3.287  proof-
   3.288    from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   3.289    from gt_ex obtain x where x: "z \<sqsubset> x" by blast
   3.290 @@ -365,11 +365,11 @@
   3.291  locale linorder_no_lb = linorder_stupid_syntax +
   3.292    assumes lt_ex: "\<exists>y. less y x"
   3.293  begin
   3.294 -lemma le_ex[noatp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
   3.295 +lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
   3.296  
   3.297  
   3.298  text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
   3.299 -lemma minf_conj[noatp]:
   3.300 +lemma minf_conj[no_atp]:
   3.301    assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   3.302    and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   3.303    shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   3.304 @@ -384,7 +384,7 @@
   3.305    thus ?thesis by blast
   3.306  qed
   3.307  
   3.308 -lemma minf_disj[noatp]:
   3.309 +lemma minf_disj[no_atp]:
   3.310    assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   3.311    and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   3.312    shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   3.313 @@ -399,7 +399,7 @@
   3.314    thus ?thesis by blast
   3.315  qed
   3.316  
   3.317 -lemma minf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   3.318 +lemma minf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   3.319  proof-
   3.320    from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   3.321    from lt_ex obtain x where x: "x \<sqsubset> z" by blast
   3.322 @@ -422,7 +422,7 @@
   3.323  context  constr_dense_linorder
   3.324  begin
   3.325  
   3.326 -lemma rinf_U[noatp]:
   3.327 +lemma rinf_U[no_atp]:
   3.328    assumes fU: "finite U"
   3.329    and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   3.330    \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   3.331 @@ -465,7 +465,7 @@
   3.332      ultimately show ?thesis by blast
   3.333    qed
   3.334  
   3.335 -theorem fr_eq[noatp]:
   3.336 +theorem fr_eq[no_atp]:
   3.337    assumes fU: "finite U"
   3.338    and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   3.339     \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   3.340 @@ -493,16 +493,16 @@
   3.341   ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
   3.342  qed
   3.343  
   3.344 -lemmas minf_thms[noatp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
   3.345 -lemmas pinf_thms[noatp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
   3.346 +lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
   3.347 +lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
   3.348  
   3.349 -lemmas nmi_thms[noatp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
   3.350 -lemmas npi_thms[noatp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
   3.351 -lemmas lin_dense_thms[noatp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
   3.352 +lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
   3.353 +lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
   3.354 +lemmas lin_dense_thms[no_atp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
   3.355  
   3.356 -lemma ferrack_axiom[noatp]: "constr_dense_linorder less_eq less between"
   3.357 +lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between"
   3.358    by (rule constr_dense_linorder_axioms)
   3.359 -lemma atoms[noatp]:
   3.360 +lemma atoms[no_atp]:
   3.361    shows "TERM (less :: 'a \<Rightarrow> _)"
   3.362      and "TERM (less_eq :: 'a \<Rightarrow> _)"
   3.363      and "TERM (op = :: 'a \<Rightarrow> _)" .
     4.1 --- a/src/HOL/Fields.thy	Wed Mar 17 19:37:44 2010 +0100
     4.2 +++ b/src/HOL/Fields.thy	Thu Mar 18 12:58:52 2010 +0100
     4.3 @@ -65,7 +65,7 @@
     4.4     ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
     4.5  by (simp add: division_ring_inverse_add mult_ac)
     4.6  
     4.7 -lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
     4.8 +lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
     4.9  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
    4.10  proof -
    4.11    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    4.12 @@ -76,7 +76,7 @@
    4.13      finally show ?thesis by (simp add: divide_inverse)
    4.14  qed
    4.15  
    4.16 -lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
    4.17 +lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
    4.18    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
    4.19  by (simp add: mult_commute [of _ c])
    4.20  
    4.21 @@ -90,7 +90,7 @@
    4.22  by (simp add: divide_inverse mult_ac)
    4.23  
    4.24  text {* These are later declared as simp rules. *}
    4.25 -lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
    4.26 +lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
    4.27  
    4.28  lemma add_frac_eq:
    4.29    assumes "y \<noteq> 0" and "z \<noteq> 0"
    4.30 @@ -106,27 +106,27 @@
    4.31  
    4.32  text{*Special Cancellation Simprules for Division*}
    4.33  
    4.34 -lemma nonzero_mult_divide_cancel_right [simp, noatp]:
    4.35 +lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
    4.36    "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
    4.37  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
    4.38  
    4.39 -lemma nonzero_mult_divide_cancel_left [simp, noatp]:
    4.40 +lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
    4.41    "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
    4.42  using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
    4.43  
    4.44 -lemma nonzero_divide_mult_cancel_right [simp, noatp]:
    4.45 +lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
    4.46    "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
    4.47  using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
    4.48  
    4.49 -lemma nonzero_divide_mult_cancel_left [simp, noatp]:
    4.50 +lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
    4.51    "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
    4.52  using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
    4.53  
    4.54 -lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
    4.55 +lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
    4.56    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
    4.57  using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
    4.58  
    4.59 -lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
    4.60 +lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
    4.61    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
    4.62  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
    4.63  
    4.64 @@ -139,7 +139,7 @@
    4.65  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
    4.66  by (simp add: divide_inverse nonzero_inverse_minus_eq)
    4.67  
    4.68 -lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
    4.69 +lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
    4.70  by (simp add: divide_inverse)
    4.71  
    4.72  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    4.73 @@ -183,7 +183,7 @@
    4.74  lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
    4.75  by (erule subst, simp)
    4.76  
    4.77 -lemmas field_eq_simps[noatp] = algebra_simps
    4.78 +lemmas field_eq_simps[no_atp] = algebra_simps
    4.79    (* pull / out*)
    4.80    add_divide_eq_iff divide_add_eq_iff
    4.81    diff_divide_eq_iff divide_diff_eq_iff
    4.82 @@ -292,18 +292,18 @@
    4.83  apply simp_all
    4.84  done
    4.85  
    4.86 -lemma divide_divide_eq_right [simp,noatp]:
    4.87 +lemma divide_divide_eq_right [simp,no_atp]:
    4.88    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
    4.89  by (simp add: divide_inverse mult_ac)
    4.90  
    4.91 -lemma divide_divide_eq_left [simp,noatp]:
    4.92 +lemma divide_divide_eq_left [simp,no_atp]:
    4.93    "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
    4.94  by (simp add: divide_inverse mult_assoc)
    4.95  
    4.96  
    4.97  subsubsection{*Special Cancellation Simprules for Division*}
    4.98  
    4.99 -lemma mult_divide_mult_cancel_left_if[simp,noatp]:
   4.100 +lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
   4.101  fixes c :: "'a :: {field,division_by_zero}"
   4.102  shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
   4.103  by (simp add: mult_divide_mult_cancel_left)
   4.104 @@ -314,7 +314,7 @@
   4.105  lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
   4.106  by (simp add: divide_inverse)
   4.107  
   4.108 -lemma divide_minus_right [simp, noatp]:
   4.109 +lemma divide_minus_right [simp, no_atp]:
   4.110    "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
   4.111  by (simp add: divide_inverse)
   4.112  
   4.113 @@ -440,7 +440,7 @@
   4.114  done
   4.115  
   4.116  text{*Both premises are essential. Consider -1 and 1.*}
   4.117 -lemma inverse_less_iff_less [simp,noatp]:
   4.118 +lemma inverse_less_iff_less [simp,no_atp]:
   4.119    "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
   4.120  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   4.121  
   4.122 @@ -448,7 +448,7 @@
   4.123    "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
   4.124  by (force simp add: order_le_less less_imp_inverse_less)
   4.125  
   4.126 -lemma inverse_le_iff_le [simp,noatp]:
   4.127 +lemma inverse_le_iff_le [simp,no_atp]:
   4.128   "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
   4.129  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   4.130  
   4.131 @@ -482,7 +482,7 @@
   4.132  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.133  done
   4.134  
   4.135 -lemma inverse_less_iff_less_neg [simp,noatp]:
   4.136 +lemma inverse_less_iff_less_neg [simp,no_atp]:
   4.137    "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
   4.138  apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.139  apply (simp del: inverse_less_iff_less 
   4.140 @@ -493,7 +493,7 @@
   4.141    "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
   4.142  by (force simp add: order_le_less less_imp_inverse_less_neg)
   4.143  
   4.144 -lemma inverse_le_iff_le_neg [simp,noatp]:
   4.145 +lemma inverse_le_iff_le_neg [simp,no_atp]:
   4.146   "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
   4.147  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   4.148  
   4.149 @@ -665,7 +665,7 @@
   4.150  (for inequations). Can be too aggressive and is therefore separate from the
   4.151  more benign @{text algebra_simps}. *}
   4.152  
   4.153 -lemmas field_simps[noatp] = field_eq_simps
   4.154 +lemmas field_simps[no_atp] = field_eq_simps
   4.155    (* multiply ineqn *)
   4.156    pos_divide_less_eq neg_divide_less_eq
   4.157    pos_less_divide_eq neg_less_divide_eq
   4.158 @@ -677,7 +677,7 @@
   4.159  sign_simps} to @{text field_simps} because the former can lead to case
   4.160  explosions. *}
   4.161  
   4.162 -lemmas sign_simps[noatp] = group_simps
   4.163 +lemmas sign_simps[no_atp] = group_simps
   4.164    zero_less_mult_iff  mult_less_0_iff
   4.165  
   4.166  (* Only works once linear arithmetic is installed:
   4.167 @@ -716,7 +716,7 @@
   4.168        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
   4.169  by (simp add: divide_inverse mult_le_0_iff)
   4.170  
   4.171 -lemma divide_eq_0_iff [simp,noatp]:
   4.172 +lemma divide_eq_0_iff [simp,no_atp]:
   4.173       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
   4.174  by (simp add: divide_inverse)
   4.175  
   4.176 @@ -756,13 +756,13 @@
   4.177  
   4.178  subsection{*Cancellation Laws for Division*}
   4.179  
   4.180 -lemma divide_cancel_right [simp,noatp]:
   4.181 +lemma divide_cancel_right [simp,no_atp]:
   4.182       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
   4.183  apply (cases "c=0", simp)
   4.184  apply (simp add: divide_inverse)
   4.185  done
   4.186  
   4.187 -lemma divide_cancel_left [simp,noatp]:
   4.188 +lemma divide_cancel_left [simp,no_atp]:
   4.189       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
   4.190  apply (cases "c=0", simp)
   4.191  apply (simp add: divide_inverse)
   4.192 @@ -772,23 +772,23 @@
   4.193  subsection {* Division and the Number One *}
   4.194  
   4.195  text{*Simplify expressions equated with 1*}
   4.196 -lemma divide_eq_1_iff [simp,noatp]:
   4.197 +lemma divide_eq_1_iff [simp,no_atp]:
   4.198       "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.199  apply (cases "b=0", simp)
   4.200  apply (simp add: right_inverse_eq)
   4.201  done
   4.202  
   4.203 -lemma one_eq_divide_iff [simp,noatp]:
   4.204 +lemma one_eq_divide_iff [simp,no_atp]:
   4.205       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.206  by (simp add: eq_commute [of 1])
   4.207  
   4.208 -lemma zero_eq_1_divide_iff [simp,noatp]:
   4.209 +lemma zero_eq_1_divide_iff [simp,no_atp]:
   4.210       "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
   4.211  apply (cases "a=0", simp)
   4.212  apply (auto simp add: nonzero_eq_divide_eq)
   4.213  done
   4.214  
   4.215 -lemma one_divide_eq_0_iff [simp,noatp]:
   4.216 +lemma one_divide_eq_0_iff [simp,no_atp]:
   4.217       "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"
   4.218  apply (cases "a=0", simp)
   4.219  apply (insert zero_neq_one [THEN not_sym])
   4.220 @@ -801,10 +801,10 @@
   4.221  lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
   4.222  lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
   4.223  
   4.224 -declare zero_less_divide_1_iff [simp,noatp]
   4.225 -declare divide_less_0_1_iff [simp,noatp]
   4.226 -declare zero_le_divide_1_iff [simp,noatp]
   4.227 -declare divide_le_0_1_iff [simp,noatp]
   4.228 +declare zero_less_divide_1_iff [simp,no_atp]
   4.229 +declare divide_less_0_1_iff [simp,no_atp]
   4.230 +declare zero_le_divide_1_iff [simp,no_atp]
   4.231 +declare divide_le_0_1_iff [simp,no_atp]
   4.232  
   4.233  
   4.234  subsection {* Ordering Rules for Division *}
   4.235 @@ -853,22 +853,22 @@
   4.236  
   4.237  text{*Simplify quotients that are compared with the value 1.*}
   4.238  
   4.239 -lemma le_divide_eq_1 [noatp]:
   4.240 +lemma le_divide_eq_1 [no_atp]:
   4.241    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.242    shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   4.243  by (auto simp add: le_divide_eq)
   4.244  
   4.245 -lemma divide_le_eq_1 [noatp]:
   4.246 +lemma divide_le_eq_1 [no_atp]:
   4.247    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.248    shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   4.249  by (auto simp add: divide_le_eq)
   4.250  
   4.251 -lemma less_divide_eq_1 [noatp]:
   4.252 +lemma less_divide_eq_1 [no_atp]:
   4.253    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.254    shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   4.255  by (auto simp add: less_divide_eq)
   4.256  
   4.257 -lemma divide_less_eq_1 [noatp]:
   4.258 +lemma divide_less_eq_1 [no_atp]:
   4.259    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.260    shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   4.261  by (auto simp add: divide_less_eq)
   4.262 @@ -876,52 +876,52 @@
   4.263  
   4.264  subsection{*Conditional Simplification Rules: No Case Splits*}
   4.265  
   4.266 -lemma le_divide_eq_1_pos [simp,noatp]:
   4.267 +lemma le_divide_eq_1_pos [simp,no_atp]:
   4.268    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.269    shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
   4.270  by (auto simp add: le_divide_eq)
   4.271  
   4.272 -lemma le_divide_eq_1_neg [simp,noatp]:
   4.273 +lemma le_divide_eq_1_neg [simp,no_atp]:
   4.274    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.275    shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
   4.276  by (auto simp add: le_divide_eq)
   4.277  
   4.278 -lemma divide_le_eq_1_pos [simp,noatp]:
   4.279 +lemma divide_le_eq_1_pos [simp,no_atp]:
   4.280    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.281    shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
   4.282  by (auto simp add: divide_le_eq)
   4.283  
   4.284 -lemma divide_le_eq_1_neg [simp,noatp]:
   4.285 +lemma divide_le_eq_1_neg [simp,no_atp]:
   4.286    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.287    shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
   4.288  by (auto simp add: divide_le_eq)
   4.289  
   4.290 -lemma less_divide_eq_1_pos [simp,noatp]:
   4.291 +lemma less_divide_eq_1_pos [simp,no_atp]:
   4.292    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.293    shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
   4.294  by (auto simp add: less_divide_eq)
   4.295  
   4.296 -lemma less_divide_eq_1_neg [simp,noatp]:
   4.297 +lemma less_divide_eq_1_neg [simp,no_atp]:
   4.298    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.299    shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
   4.300  by (auto simp add: less_divide_eq)
   4.301  
   4.302 -lemma divide_less_eq_1_pos [simp,noatp]:
   4.303 +lemma divide_less_eq_1_pos [simp,no_atp]:
   4.304    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.305    shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
   4.306  by (auto simp add: divide_less_eq)
   4.307  
   4.308 -lemma divide_less_eq_1_neg [simp,noatp]:
   4.309 +lemma divide_less_eq_1_neg [simp,no_atp]:
   4.310    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.311    shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
   4.312  by (auto simp add: divide_less_eq)
   4.313  
   4.314 -lemma eq_divide_eq_1 [simp,noatp]:
   4.315 +lemma eq_divide_eq_1 [simp,no_atp]:
   4.316    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.317    shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
   4.318  by (auto simp add: eq_divide_eq)
   4.319  
   4.320 -lemma divide_eq_eq_1 [simp,noatp]:
   4.321 +lemma divide_eq_eq_1 [simp,no_atp]:
   4.322    fixes a :: "'a :: {linordered_field,division_by_zero}"
   4.323    shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
   4.324  by (auto simp add: divide_eq_eq)
     5.1 --- a/src/HOL/Finite_Set.thy	Wed Mar 17 19:37:44 2010 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Thu Mar 18 12:58:52 2010 +0100
     5.3 @@ -524,13 +524,13 @@
     5.4  
     5.5  end
     5.6  
     5.7 -lemma UNIV_unit [noatp]:
     5.8 +lemma UNIV_unit [no_atp]:
     5.9    "UNIV = {()}" by auto
    5.10  
    5.11  instance unit :: finite proof
    5.12  qed (simp add: UNIV_unit)
    5.13  
    5.14 -lemma UNIV_bool [noatp]:
    5.15 +lemma UNIV_bool [no_atp]:
    5.16    "UNIV = {False, True}" by auto
    5.17  
    5.18  instance bool :: finite proof
    5.19 @@ -1779,7 +1779,7 @@
    5.20    "card A > 0 \<Longrightarrow> finite A"
    5.21    by (rule ccontr) simp
    5.22  
    5.23 -lemma card_0_eq [simp, noatp]:
    5.24 +lemma card_0_eq [simp, no_atp]:
    5.25    "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
    5.26    by (auto dest: mk_disjoint_insert)
    5.27  
    5.28 @@ -2109,8 +2109,8 @@
    5.29    show False by simp (blast dest: Suc_neq_Zero surjD)
    5.30  qed
    5.31  
    5.32 -(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
    5.33 -lemma infinite_UNIV_char_0[noatp]:
    5.34 +(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
    5.35 +lemma infinite_UNIV_char_0[no_atp]:
    5.36    "\<not> finite (UNIV::'a::semiring_char_0 set)"
    5.37  proof
    5.38    assume "finite (UNIV::'a set)"
     6.1 --- a/src/HOL/Groups.thy	Wed Mar 17 19:37:44 2010 +0100
     6.2 +++ b/src/HOL/Groups.thy	Thu Mar 18 12:58:52 2010 +0100
     6.3 @@ -437,7 +437,7 @@
     6.4  
     6.5  (* FIXME: duplicates right_minus_eq from class group_add *)
     6.6  (* but only this one is declared as a simp rule. *)
     6.7 -lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
     6.8 +lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
     6.9  by (simp add: algebra_simps)
    6.10  
    6.11  end
    6.12 @@ -772,12 +772,12 @@
    6.13  by (simp add: algebra_simps)
    6.14  
    6.15  text{*Legacy - use @{text algebra_simps} *}
    6.16 -lemmas group_simps[noatp] = algebra_simps
    6.17 +lemmas group_simps[no_atp] = algebra_simps
    6.18  
    6.19  end
    6.20  
    6.21  text{*Legacy - use @{text algebra_simps} *}
    6.22 -lemmas group_simps[noatp] = algebra_simps
    6.23 +lemmas group_simps[no_atp] = algebra_simps
    6.24  
    6.25  class linordered_ab_semigroup_add =
    6.26    linorder + ordered_ab_semigroup_add
    6.27 @@ -1054,7 +1054,7 @@
    6.28  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
    6.29  by simp
    6.30  
    6.31 -lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    6.32 +lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    6.33  proof -
    6.34    have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
    6.35    thus ?thesis by simp
    6.36 @@ -1201,7 +1201,7 @@
    6.37  
    6.38  subsection {* Tools setup *}
    6.39  
    6.40 -lemma add_mono_thms_linordered_semiring [noatp]:
    6.41 +lemma add_mono_thms_linordered_semiring [no_atp]:
    6.42    fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
    6.43    shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    6.44      and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    6.45 @@ -1209,7 +1209,7 @@
    6.46      and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
    6.47  by (rule add_mono, clarify+)+
    6.48  
    6.49 -lemma add_mono_thms_linordered_field [noatp]:
    6.50 +lemma add_mono_thms_linordered_field [no_atp]:
    6.51    fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
    6.52    shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
    6.53      and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
    6.54 @@ -1220,8 +1220,8 @@
    6.55    add_less_le_mono add_le_less_mono add_strict_mono)
    6.56  
    6.57  text{*Simplification of @{term "x-y < 0"}, etc.*}
    6.58 -lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
    6.59 -lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
    6.60 +lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
    6.61 +lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
    6.62  
    6.63  ML {*
    6.64  structure ab_group_add_cancel = Abel_Cancel
     7.1 --- a/src/HOL/HOL.thy	Wed Mar 17 19:37:44 2010 +0100
     7.2 +++ b/src/HOL/HOL.thy	Thu Mar 18 12:58:52 2010 +0100
     7.3 @@ -23,7 +23,6 @@
     7.4    "~~/src/Tools/coherent.ML"
     7.5    "~~/src/Tools/eqsubst.ML"
     7.6    "~~/src/Provers/quantifier1.ML"
     7.7 -  "Tools/res_blacklist.ML"
     7.8    ("Tools/simpdata.ML")
     7.9    "~~/src/Tools/random_word.ML"
    7.10    "~~/src/Tools/atomize_elim.ML"
    7.11 @@ -35,8 +34,6 @@
    7.12  
    7.13  setup {* Intuitionistic.method_setup @{binding iprover} *}
    7.14  
    7.15 -setup Res_Blacklist.setup
    7.16 -
    7.17  
    7.18  subsection {* Primitive logic *}
    7.19  
    7.20 @@ -794,6 +791,25 @@
    7.21  
    7.22  subsection {* Package setup *}
    7.23  
    7.24 +subsubsection {* Sledgehammer setup *}
    7.25 +
    7.26 +text {*
    7.27 +Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
    7.28 +that are prolific (match too many equality or membership literals) and relate to
    7.29 +seldom-used facts. Some duplicate other rules.
    7.30 +*}
    7.31 +
    7.32 +ML {*
    7.33 +structure No_ATPs = Named_Thms
    7.34 +(
    7.35 +  val name = "no_atp"
    7.36 +  val description = "theorems that should be avoided by Sledgehammer"
    7.37 +)
    7.38 +*}
    7.39 +
    7.40 +setup {* No_ATPs.setup *}
    7.41 +
    7.42 +
    7.43  subsubsection {* Classical Reasoner setup *}
    7.44  
    7.45  lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
    7.46 @@ -1041,7 +1057,7 @@
    7.47  lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
    7.48  lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
    7.49  
    7.50 -declare All_def [noatp]
    7.51 +declare All_def [no_atp]
    7.52  
    7.53  lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
    7.54  lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
    7.55 @@ -1088,7 +1104,7 @@
    7.56  lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    7.57  by (simplesubst split_if, blast)
    7.58  
    7.59 -lemmas if_splits [noatp] = split_if split_if_asm
    7.60 +lemmas if_splits [no_atp] = split_if split_if_asm
    7.61  
    7.62  lemma if_cancel: "(if c then x else x) = x"
    7.63  by (simplesubst split_if, blast)
     8.1 --- a/src/HOL/Int.thy	Wed Mar 17 19:37:44 2010 +0100
     8.2 +++ b/src/HOL/Int.thy	Thu Mar 18 12:58:52 2010 +0100
     8.3 @@ -86,7 +86,7 @@
     8.4  
     8.5  text{*Reduces equality on abstractions to equality on representatives:
     8.6    @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
     8.7 -declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
     8.8 +declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
     8.9  
    8.10  text{*Case analysis on the representation of an integer as an equivalence
    8.11        class of pairs of naturals.*}
    8.12 @@ -522,7 +522,7 @@
    8.13        It is proved here because attribute @{text arith_split} is not available
    8.14        in theory @{text Rings}.
    8.15        But is it really better than just rewriting with @{text abs_if}?*}
    8.16 -lemma abs_split [arith_split,noatp]:
    8.17 +lemma abs_split [arith_split,no_atp]:
    8.18       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
    8.19  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    8.20  
    8.21 @@ -1874,16 +1874,16 @@
    8.22  
    8.23  text{*These are actually for fields, like real: but where else to put them?*}
    8.24  
    8.25 -lemmas zero_less_divide_iff_number_of [simp, noatp] =
    8.26 +lemmas zero_less_divide_iff_number_of [simp, no_atp] =
    8.27    zero_less_divide_iff [of "number_of w", standard]
    8.28  
    8.29 -lemmas divide_less_0_iff_number_of [simp, noatp] =
    8.30 +lemmas divide_less_0_iff_number_of [simp, no_atp] =
    8.31    divide_less_0_iff [of "number_of w", standard]
    8.32  
    8.33 -lemmas zero_le_divide_iff_number_of [simp, noatp] =
    8.34 +lemmas zero_le_divide_iff_number_of [simp, no_atp] =
    8.35    zero_le_divide_iff [of "number_of w", standard]
    8.36  
    8.37 -lemmas divide_le_0_iff_number_of [simp, noatp] =
    8.38 +lemmas divide_le_0_iff_number_of [simp, no_atp] =
    8.39    divide_le_0_iff [of "number_of w", standard]
    8.40  
    8.41  
    8.42 @@ -1896,53 +1896,53 @@
    8.43  text {*These laws simplify inequalities, moving unary minus from a term
    8.44  into the literal.*}
    8.45  
    8.46 -lemmas less_minus_iff_number_of [simp, noatp] =
    8.47 +lemmas less_minus_iff_number_of [simp, no_atp] =
    8.48    less_minus_iff [of "number_of v", standard]
    8.49  
    8.50 -lemmas le_minus_iff_number_of [simp, noatp] =
    8.51 +lemmas le_minus_iff_number_of [simp, no_atp] =
    8.52    le_minus_iff [of "number_of v", standard]
    8.53  
    8.54 -lemmas equation_minus_iff_number_of [simp, noatp] =
    8.55 +lemmas equation_minus_iff_number_of [simp, no_atp] =
    8.56    equation_minus_iff [of "number_of v", standard]
    8.57  
    8.58 -lemmas minus_less_iff_number_of [simp, noatp] =
    8.59 +lemmas minus_less_iff_number_of [simp, no_atp] =
    8.60    minus_less_iff [of _ "number_of v", standard]
    8.61  
    8.62 -lemmas minus_le_iff_number_of [simp, noatp] =
    8.63 +lemmas minus_le_iff_number_of [simp, no_atp] =
    8.64    minus_le_iff [of _ "number_of v", standard]
    8.65  
    8.66 -lemmas minus_equation_iff_number_of [simp, noatp] =
    8.67 +lemmas minus_equation_iff_number_of [simp, no_atp] =
    8.68    minus_equation_iff [of _ "number_of v", standard]
    8.69  
    8.70  
    8.71  text{*To Simplify Inequalities Where One Side is the Constant 1*}
    8.72  
    8.73 -lemma less_minus_iff_1 [simp,noatp]:
    8.74 +lemma less_minus_iff_1 [simp,no_atp]:
    8.75    fixes b::"'b::{linordered_idom,number_ring}"
    8.76    shows "(1 < - b) = (b < -1)"
    8.77  by auto
    8.78  
    8.79 -lemma le_minus_iff_1 [simp,noatp]:
    8.80 +lemma le_minus_iff_1 [simp,no_atp]:
    8.81    fixes b::"'b::{linordered_idom,number_ring}"
    8.82    shows "(1 \<le> - b) = (b \<le> -1)"
    8.83  by auto
    8.84  
    8.85 -lemma equation_minus_iff_1 [simp,noatp]:
    8.86 +lemma equation_minus_iff_1 [simp,no_atp]:
    8.87    fixes b::"'b::number_ring"
    8.88    shows "(1 = - b) = (b = -1)"
    8.89  by (subst equation_minus_iff, auto)
    8.90  
    8.91 -lemma minus_less_iff_1 [simp,noatp]:
    8.92 +lemma minus_less_iff_1 [simp,no_atp]:
    8.93    fixes a::"'b::{linordered_idom,number_ring}"
    8.94    shows "(- a < 1) = (-1 < a)"
    8.95  by auto
    8.96  
    8.97 -lemma minus_le_iff_1 [simp,noatp]:
    8.98 +lemma minus_le_iff_1 [simp,no_atp]:
    8.99    fixes a::"'b::{linordered_idom,number_ring}"
   8.100    shows "(- a \<le> 1) = (-1 \<le> a)"
   8.101  by auto
   8.102  
   8.103 -lemma minus_equation_iff_1 [simp,noatp]:
   8.104 +lemma minus_equation_iff_1 [simp,no_atp]:
   8.105    fixes a::"'b::number_ring"
   8.106    shows "(- a = 1) = (a = -1)"
   8.107  by (subst minus_equation_iff, auto)
   8.108 @@ -1950,16 +1950,16 @@
   8.109  
   8.110  text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
   8.111  
   8.112 -lemmas mult_less_cancel_left_number_of [simp, noatp] =
   8.113 +lemmas mult_less_cancel_left_number_of [simp, no_atp] =
   8.114    mult_less_cancel_left [of "number_of v", standard]
   8.115  
   8.116 -lemmas mult_less_cancel_right_number_of [simp, noatp] =
   8.117 +lemmas mult_less_cancel_right_number_of [simp, no_atp] =
   8.118    mult_less_cancel_right [of _ "number_of v", standard]
   8.119  
   8.120 -lemmas mult_le_cancel_left_number_of [simp, noatp] =
   8.121 +lemmas mult_le_cancel_left_number_of [simp, no_atp] =
   8.122    mult_le_cancel_left [of "number_of v", standard]
   8.123  
   8.124 -lemmas mult_le_cancel_right_number_of [simp, noatp] =
   8.125 +lemmas mult_le_cancel_right_number_of [simp, no_atp] =
   8.126    mult_le_cancel_right [of _ "number_of v", standard]
   8.127  
   8.128  
     9.1 --- a/src/HOL/IsaMakefile	Wed Mar 17 19:37:44 2010 +0100
     9.2 +++ b/src/HOL/IsaMakefile	Thu Mar 18 12:58:52 2010 +0100
     9.3 @@ -314,7 +314,6 @@
     9.4    Tools/Quotient/quotient_term.ML \
     9.5    Tools/Quotient/quotient_typ.ML \
     9.6    Tools/recdef.ML \
     9.7 -  Tools/res_blacklist.ML \
     9.8    Tools/Sledgehammer/metis_tactics.ML \
     9.9    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
    9.10    Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
    10.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 17 19:37:44 2010 +0100
    10.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 18 12:58:52 2010 +0100
    10.3 @@ -163,16 +163,16 @@
    10.4  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
    10.5  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
    10.6  
    10.7 -lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
    10.8 +lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x"
    10.9    by (simp add: pprt_def sup_aci sup_absorb1)
   10.10  
   10.11 -lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   10.12 +lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   10.13    by (simp add: nprt_def inf_aci inf_absorb1)
   10.14  
   10.15 -lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   10.16 +lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   10.17    by (simp add: pprt_def sup_aci sup_absorb2)
   10.18  
   10.19 -lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   10.20 +lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   10.21    by (simp add: nprt_def inf_aci inf_absorb2)
   10.22  
   10.23  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
   10.24 @@ -197,10 +197,10 @@
   10.25  apply (erule sup_0_imp_0)
   10.26  done
   10.27  
   10.28 -lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
   10.29 +lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
   10.30  by (rule, erule inf_0_imp_0) simp
   10.31  
   10.32 -lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
   10.33 +lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
   10.34  by (rule, erule sup_0_imp_0) simp
   10.35  
   10.36  lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   10.37 @@ -295,10 +295,10 @@
   10.38  lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   10.39  unfolding le_iff_inf by (simp add: nprt_def inf_commute)
   10.40  
   10.41 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   10.42 +lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   10.43  unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
   10.44  
   10.45 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   10.46 +lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   10.47  unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
   10.48  
   10.49  end
    11.1 --- a/src/HOL/List.thy	Wed Mar 17 19:37:44 2010 +0100
    11.2 +++ b/src/HOL/List.thy	Thu Mar 18 12:58:52 2010 +0100
    11.3 @@ -582,7 +582,7 @@
    11.4  lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
    11.5  by (induct xs) auto
    11.6  
    11.7 -lemma append_eq_append_conv [simp, noatp]:
    11.8 +lemma append_eq_append_conv [simp, no_atp]:
    11.9   "length xs = length ys \<or> length us = length vs
   11.10   ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   11.11  apply (induct xs arbitrary: ys)
   11.12 @@ -614,7 +614,7 @@
   11.13  lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
   11.14  using append_same_eq [of "[]"] by auto
   11.15  
   11.16 -lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   11.17 +lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   11.18  by (induct xs) auto
   11.19  
   11.20  lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
   11.21 @@ -3928,10 +3928,10 @@
   11.22    for A :: "'a set"
   11.23  where
   11.24      Nil [intro!]: "[]: lists A"
   11.25 -  | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
   11.26 -
   11.27 -inductive_cases listsE [elim!,noatp]: "x#l : lists A"
   11.28 -inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
   11.29 +  | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
   11.30 +
   11.31 +inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
   11.32 +inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
   11.33  
   11.34  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
   11.35  by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
   11.36 @@ -3966,15 +3966,15 @@
   11.37  
   11.38  lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
   11.39  
   11.40 -lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
   11.41 +lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
   11.42  by (rule in_listsp_conv_set [THEN iffD1])
   11.43  
   11.44 -lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
   11.45 -
   11.46 -lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
   11.47 +lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
   11.48 +
   11.49 +lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
   11.50  by (rule in_listsp_conv_set [THEN iffD2])
   11.51  
   11.52 -lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
   11.53 +lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
   11.54  
   11.55  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
   11.56  by auto
    12.1 --- a/src/HOL/Nat.thy	Wed Mar 17 19:37:44 2010 +0100
    12.2 +++ b/src/HOL/Nat.thy	Thu Mar 18 12:58:52 2010 +0100
    12.3 @@ -320,7 +320,7 @@
    12.4     apply auto
    12.5    done
    12.6  
    12.7 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
    12.8 +lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
    12.9    apply (rule trans)
   12.10    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   12.11    done
   12.12 @@ -480,7 +480,7 @@
   12.13  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   12.14    by (simp add: less_Suc_eq)
   12.15  
   12.16 -lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
   12.17 +lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
   12.18    unfolding One_nat_def by (rule less_Suc0)
   12.19  
   12.20  lemma Suc_mono: "m < n ==> Suc m < Suc n"
   12.21 @@ -648,7 +648,7 @@
   12.22  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   12.23  by (fast intro: not0_implies_Suc)
   12.24  
   12.25 -lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   12.26 +lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   12.27  using neq0_conv by blast
   12.28  
   12.29  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   12.30 @@ -1279,10 +1279,10 @@
   12.31  
   12.32  text{*Special cases where either operand is zero*}
   12.33  
   12.34 -lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   12.35 +lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   12.36    by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
   12.37  
   12.38 -lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   12.39 +lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   12.40    by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
   12.41  
   12.42  lemma inj_of_nat: "inj of_nat"
   12.43 @@ -1327,7 +1327,7 @@
   12.44  lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
   12.45    by (rule of_nat_le_iff [of 0, simplified])
   12.46  
   12.47 -lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   12.48 +lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   12.49    by (rule of_nat_le_iff [of _ 0, simplified])
   12.50  
   12.51  lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
    13.1 --- a/src/HOL/Orderings.thy	Wed Mar 17 19:37:44 2010 +0100
    13.2 +++ b/src/HOL/Orderings.thy	Thu Mar 18 12:58:52 2010 +0100
    13.3 @@ -293,11 +293,11 @@
    13.4    "max x y < z \<longleftrightarrow> x < z \<and> y < z"
    13.5  unfolding max_def le_less using less_linear by (auto intro: less_trans)
    13.6  
    13.7 -lemma split_min [noatp]:
    13.8 +lemma split_min [no_atp]:
    13.9    "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   13.10  by (simp add: min_def)
   13.11  
   13.12 -lemma split_max [noatp]:
   13.13 +lemma split_max [no_atp]:
   13.14    "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   13.15  by (simp add: max_def)
   13.16  
    14.1 --- a/src/HOL/Power.thy	Wed Mar 17 19:37:44 2010 +0100
    14.2 +++ b/src/HOL/Power.thy	Thu Mar 18 12:58:52 2010 +0100
    14.3 @@ -334,7 +334,7 @@
    14.4    "abs ((-a) ^ n) = abs (a ^ n)"
    14.5    by (simp add: power_abs)
    14.6  
    14.7 -lemma zero_less_power_abs_iff [simp, noatp]:
    14.8 +lemma zero_less_power_abs_iff [simp, no_atp]:
    14.9    "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   14.10  proof (induct n)
   14.11    case 0 show ?case by simp
    15.1 --- a/src/HOL/Product_Type.thy	Wed Mar 17 19:37:44 2010 +0100
    15.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 18 12:58:52 2010 +0100
    15.3 @@ -46,7 +46,7 @@
    15.4  where
    15.5    "() = Abs_unit True"
    15.6  
    15.7 -lemma unit_eq [noatp]: "u = ()"
    15.8 +lemma unit_eq [no_atp]: "u = ()"
    15.9    by (induct u) (simp add: unit_def Unity_def)
   15.10  
   15.11  text {*
   15.12 @@ -78,7 +78,7 @@
   15.13    f} rather than by @{term [source] "%u. f ()"}.
   15.14  *}
   15.15  
   15.16 -lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   15.17 +lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
   15.18    by (rule ext) simp
   15.19  
   15.20  instantiation unit :: default
   15.21 @@ -497,7 +497,7 @@
   15.22  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   15.23    by (subst surjective_pairing, rule split_conv)
   15.24  
   15.25 -lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   15.26 +lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   15.27    -- {* For use with @{text split} and the Simplifier. *}
   15.28    by (insert surj_pair [of p], clarify, simp)
   15.29  
   15.30 @@ -508,7 +508,7 @@
   15.31    current goal contains one of those constants.
   15.32  *}
   15.33  
   15.34 -lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   15.35 +lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   15.36  by (subst split_split, simp)
   15.37  
   15.38  
   15.39 @@ -582,10 +582,10 @@
   15.40    Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
   15.41  *}
   15.42  
   15.43 -lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   15.44 +lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   15.45    by (rule ext) fast
   15.46  
   15.47 -lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   15.48 +lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   15.49    by (rule ext) fast
   15.50  
   15.51  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   15.52 @@ -947,11 +947,11 @@
   15.53    -- {* Suggested by Pierre Chartier *}
   15.54    by blast
   15.55  
   15.56 -lemma split_paired_Ball_Sigma [simp,noatp]:
   15.57 +lemma split_paired_Ball_Sigma [simp,no_atp]:
   15.58      "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   15.59    by blast
   15.60  
   15.61 -lemma split_paired_Bex_Sigma [simp,noatp]:
   15.62 +lemma split_paired_Bex_Sigma [simp,no_atp]:
   15.63      "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   15.64    by blast
   15.65  
    16.1 --- a/src/HOL/Relation.thy	Wed Mar 17 19:37:44 2010 +0100
    16.2 +++ b/src/HOL/Relation.thy	Thu Mar 18 12:58:52 2010 +0100
    16.3 @@ -121,7 +121,7 @@
    16.4  lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
    16.5  by (simp add: Id_on_def)
    16.6  
    16.7 -lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
    16.8 +lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
    16.9  by (rule Id_on_eqI) (rule refl)
   16.10  
   16.11  lemma Id_onE [elim!]:
   16.12 @@ -361,7 +361,7 @@
   16.13  
   16.14  subsection {* Domain *}
   16.15  
   16.16 -declare Domain_def [noatp]
   16.17 +declare Domain_def [no_atp]
   16.18  
   16.19  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   16.20  by (unfold Domain_def) blast
   16.21 @@ -484,7 +484,7 @@
   16.22  
   16.23  subsection {* Image of a set under a relation *}
   16.24  
   16.25 -declare Image_def [noatp]
   16.26 +declare Image_def [no_atp]
   16.27  
   16.28  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   16.29  by (simp add: Image_def)
   16.30 @@ -495,7 +495,7 @@
   16.31  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   16.32  by (rule Image_iff [THEN trans]) simp
   16.33  
   16.34 -lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
   16.35 +lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
   16.36  by (unfold Image_def) blast
   16.37  
   16.38  lemma ImageE [elim!]:
    17.1 --- a/src/HOL/Rings.thy	Wed Mar 17 19:37:44 2010 +0100
    17.2 +++ b/src/HOL/Rings.thy	Thu Mar 18 12:58:52 2010 +0100
    17.3 @@ -127,7 +127,7 @@
    17.4    then show ?thesis ..
    17.5  qed
    17.6  
    17.7 -lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
    17.8 +lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
    17.9  by (auto intro: dvd_refl elim!: dvdE)
   17.10  
   17.11  lemma dvd_0_right [iff]: "a dvd 0"
   17.12 @@ -221,8 +221,8 @@
   17.13  by (rule minus_unique) (simp add: right_distrib [symmetric]) 
   17.14  
   17.15  text{*Extract signs from products*}
   17.16 -lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
   17.17 -lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
   17.18 +lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
   17.19 +lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
   17.20  
   17.21  lemma minus_mult_minus [simp]: "- a * - b = a * b"
   17.22  by simp
   17.23 @@ -236,11 +236,11 @@
   17.24  lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
   17.25  by (simp add: left_distrib diff_minus)
   17.26  
   17.27 -lemmas ring_distribs[noatp] =
   17.28 +lemmas ring_distribs[no_atp] =
   17.29    right_distrib left_distrib left_diff_distrib right_diff_distrib
   17.30  
   17.31  text{*Legacy - use @{text algebra_simps} *}
   17.32 -lemmas ring_simps[noatp] = algebra_simps
   17.33 +lemmas ring_simps[no_atp] = algebra_simps
   17.34  
   17.35  lemma eq_add_iff1:
   17.36    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
   17.37 @@ -252,7 +252,7 @@
   17.38  
   17.39  end
   17.40  
   17.41 -lemmas ring_distribs[noatp] =
   17.42 +lemmas ring_distribs[no_atp] =
   17.43    right_distrib left_distrib left_diff_distrib right_diff_distrib
   17.44  
   17.45  class comm_ring = comm_semiring + ab_group_add
   17.46 @@ -319,7 +319,7 @@
   17.47  qed
   17.48  
   17.49  text{*Cancellation of equalities with a common factor*}
   17.50 -lemma mult_cancel_right [simp, noatp]:
   17.51 +lemma mult_cancel_right [simp, no_atp]:
   17.52    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   17.53  proof -
   17.54    have "(a * c = b * c) = ((a - b) * c = 0)"
   17.55 @@ -327,7 +327,7 @@
   17.56    thus ?thesis by (simp add: disj_commute)
   17.57  qed
   17.58  
   17.59 -lemma mult_cancel_left [simp, noatp]:
   17.60 +lemma mult_cancel_left [simp, no_atp]:
   17.61    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   17.62  proof -
   17.63    have "(c * a = c * b) = (c * (a - b) = 0)"
   17.64 @@ -743,7 +743,7 @@
   17.65  subclass ordered_ab_group_add ..
   17.66  
   17.67  text{*Legacy - use @{text algebra_simps} *}
   17.68 -lemmas ring_simps[noatp] = algebra_simps
   17.69 +lemmas ring_simps[no_atp] = algebra_simps
   17.70  
   17.71  lemma less_add_iff1:
   17.72    "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   17.73 @@ -950,7 +950,7 @@
   17.74  end
   17.75  
   17.76  text{*Legacy - use @{text algebra_simps} *}
   17.77 -lemmas ring_simps[noatp] = algebra_simps
   17.78 +lemmas ring_simps[no_atp] = algebra_simps
   17.79  
   17.80  lemmas mult_sign_intros =
   17.81    mult_nonneg_nonneg mult_nonneg_nonpos
   17.82 @@ -1099,7 +1099,7 @@
   17.83  
   17.84  text {* Simprules for comparisons where common factors can be cancelled. *}
   17.85  
   17.86 -lemmas mult_compare_simps[noatp] =
   17.87 +lemmas mult_compare_simps[no_atp] =
   17.88      mult_le_cancel_right mult_le_cancel_left
   17.89      mult_le_cancel_right1 mult_le_cancel_right2
   17.90      mult_le_cancel_left1 mult_le_cancel_left2
   17.91 @@ -1180,7 +1180,7 @@
   17.92    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   17.93  qed
   17.94  
   17.95 -lemmas eq_minus_self_iff[noatp] = equal_neg_zero
   17.96 +lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
   17.97  
   17.98  lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
   17.99    unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
    18.1 --- a/src/HOL/Set.thy	Wed Mar 17 19:37:44 2010 +0100
    18.2 +++ b/src/HOL/Set.thy	Thu Mar 18 12:58:52 2010 +0100
    18.3 @@ -462,7 +462,7 @@
    18.4    unfolding mem_def by (erule le_funE, erule le_boolE)
    18.5    -- {* Rule in Modus Ponens style. *}
    18.6  
    18.7 -lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
    18.8 +lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
    18.9    -- {* The same, with reversed premises for use with @{text erule} --
   18.10        cf @{text rev_mp}. *}
   18.11    by (rule subsetD)
   18.12 @@ -471,13 +471,13 @@
   18.13    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
   18.14  *}
   18.15  
   18.16 -lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   18.17 +lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   18.18    -- {* Classical elimination rule. *}
   18.19    unfolding mem_def by (blast dest: le_funE le_boolE)
   18.20  
   18.21 -lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   18.22 +lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   18.23  
   18.24 -lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   18.25 +lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   18.26    by blast
   18.27  
   18.28  lemma subset_refl [simp]: "A \<subseteq> A"
   18.29 @@ -791,11 +791,11 @@
   18.30  
   18.31  subsubsection {* Singletons, using insert *}
   18.32  
   18.33 -lemma singletonI [intro!,noatp]: "a : {a}"
   18.34 +lemma singletonI [intro!,no_atp]: "a : {a}"
   18.35      -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   18.36    by (rule insertI1)
   18.37  
   18.38 -lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
   18.39 +lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
   18.40    by blast
   18.41  
   18.42  lemmas singletonE = singletonD [elim_format]
   18.43 @@ -806,11 +806,11 @@
   18.44  lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   18.45    by blast
   18.46  
   18.47 -lemma singleton_insert_inj_eq [iff,noatp]:
   18.48 +lemma singleton_insert_inj_eq [iff,no_atp]:
   18.49       "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   18.50    by blast
   18.51  
   18.52 -lemma singleton_insert_inj_eq' [iff,noatp]:
   18.53 +lemma singleton_insert_inj_eq' [iff,no_atp]:
   18.54       "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   18.55    by blast
   18.56  
   18.57 @@ -837,7 +837,7 @@
   18.58  *}
   18.59  
   18.60  definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
   18.61 -  image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
   18.62 +  image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
   18.63  
   18.64  abbreviation
   18.65    range :: "('a => 'b) => 'b set" where -- "of function"
   18.66 @@ -942,10 +942,10 @@
   18.67  
   18.68  subsubsection {* The ``proper subset'' relation *}
   18.69  
   18.70 -lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   18.71 +lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   18.72    by (unfold less_le) blast
   18.73  
   18.74 -lemma psubsetE [elim!,noatp]: 
   18.75 +lemma psubsetE [elim!,no_atp]: 
   18.76      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   18.77    by (unfold less_le) blast
   18.78  
   18.79 @@ -1102,12 +1102,12 @@
   18.80  lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   18.81    by blast
   18.82  
   18.83 -lemma insert_disjoint [simp,noatp]:
   18.84 +lemma insert_disjoint [simp,no_atp]:
   18.85   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
   18.86   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
   18.87    by auto
   18.88  
   18.89 -lemma disjoint_insert [simp,noatp]:
   18.90 +lemma disjoint_insert [simp,no_atp]:
   18.91   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
   18.92   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   18.93    by auto
   18.94 @@ -1139,7 +1139,7 @@
   18.95  by blast
   18.96  
   18.97  
   18.98 -lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
   18.99 +lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
  18.100    -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
  18.101        with its implicit quantifier and conjunction.  Also image enjoys better
  18.102        equational properties than does the RHS. *}
  18.103 @@ -1156,7 +1156,7 @@
  18.104  
  18.105  text {* \medskip @{text range}. *}
  18.106  
  18.107 -lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
  18.108 +lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
  18.109    by auto
  18.110  
  18.111  lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
  18.112 @@ -1213,7 +1213,7 @@
  18.113  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
  18.114    by blast
  18.115  
  18.116 -lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  18.117 +lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  18.118    by blast
  18.119  
  18.120  lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  18.121 @@ -1376,7 +1376,7 @@
  18.122  lemma Diff_eq: "A - B = A \<inter> (-B)"
  18.123    by blast
  18.124  
  18.125 -lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
  18.126 +lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
  18.127    by blast
  18.128  
  18.129  lemma Diff_cancel [simp]: "A - A = {}"
  18.130 @@ -1397,7 +1397,7 @@
  18.131  lemma Diff_UNIV [simp]: "A - UNIV = {}"
  18.132    by blast
  18.133  
  18.134 -lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
  18.135 +lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
  18.136    by blast
  18.137  
  18.138  lemma Diff_insert: "A - insert a B = A - B - {a}"
  18.139 @@ -1639,7 +1639,7 @@
  18.140    -- {* monotonicity *}
  18.141    by blast
  18.142  
  18.143 -lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  18.144 +lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  18.145  by (blast intro: sym)
  18.146  
  18.147  lemma image_vimage_subset: "f ` (f -` A) <= A"
    19.1 --- a/src/HOL/SetInterval.thy	Wed Mar 17 19:37:44 2010 +0100
    19.2 +++ b/src/HOL/SetInterval.thy	Thu Mar 18 12:58:52 2010 +0100
    19.3 @@ -165,19 +165,19 @@
    19.4  context ord
    19.5  begin
    19.6  
    19.7 -lemma greaterThanLessThan_iff [simp,noatp]:
    19.8 +lemma greaterThanLessThan_iff [simp,no_atp]:
    19.9    "(i : {l<..<u}) = (l < i & i < u)"
   19.10  by (simp add: greaterThanLessThan_def)
   19.11  
   19.12 -lemma atLeastLessThan_iff [simp,noatp]:
   19.13 +lemma atLeastLessThan_iff [simp,no_atp]:
   19.14    "(i : {l..<u}) = (l <= i & i < u)"
   19.15  by (simp add: atLeastLessThan_def)
   19.16  
   19.17 -lemma greaterThanAtMost_iff [simp,noatp]:
   19.18 +lemma greaterThanAtMost_iff [simp,no_atp]:
   19.19    "(i : {l<..u}) = (l < i & i <= u)"
   19.20  by (simp add: greaterThanAtMost_def)
   19.21  
   19.22 -lemma atLeastAtMost_iff [simp,noatp]:
   19.23 +lemma atLeastAtMost_iff [simp,no_atp]:
   19.24    "(i : {l..u}) = (l <= i & i <= u)"
   19.25  by (simp add: atLeastAtMost_def)
   19.26  
   19.27 @@ -844,7 +844,7 @@
   19.28  
   19.29  subsubsection {* Some Subset Conditions *}
   19.30  
   19.31 -lemma ivl_subset [simp,noatp]:
   19.32 +lemma ivl_subset [simp,no_atp]:
   19.33   "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
   19.34  apply(auto simp:linorder_not_le)
   19.35  apply(rule ccontr)
    20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Mar 17 19:37:44 2010 +0100
    20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Mar 18 12:58:52 2010 +0100
    20.3 @@ -412,10 +412,11 @@
    20.4  fun name_thm_pairs ctxt =
    20.5    let
    20.6      val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
    20.7 -    fun blacklisted (_, th) =
    20.8 -      run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
    20.9 +    val blacklist =
   20.10 +      if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
   20.11 +    fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
   20.12    in
   20.13 -    filter_out blacklisted
   20.14 +    filter_out is_blacklisted
   20.15        (fold add_single_names singles (fold add_multi_names mults []))
   20.16    end;
   20.17  
    21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Mar 17 19:37:44 2010 +0100
    21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Mar 18 12:58:52 2010 +0100
    21.3 @@ -326,7 +326,7 @@
    21.4  
    21.5  val multi_base_blacklist =
    21.6    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
    21.7 -   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "noatp" *)
    21.8 +   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "no_atp" *)
    21.9  
   21.10  (*Keep the full complexity of the original name*)
   21.11  fun flatten_name s = space_implode "_X" (Long_Name.explode s);
    22.1 --- a/src/HOL/Tools/res_blacklist.ML	Wed Mar 17 19:37:44 2010 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,43 +0,0 @@
    22.4 -(*  Title:      HOL/Tools/res_blacklist.ML
    22.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.6 -    Author:     Makarius
    22.7 -
    22.8 -Theorems blacklisted to sledgehammer.  These theorems typically
    22.9 -produce clauses that are prolific (match too many equality or
   22.10 -membership literals) and relate to seldom-used facts.  Some duplicate
   22.11 -other rules.
   22.12 -*)
   22.13 -
   22.14 -signature RES_BLACKLIST =
   22.15 -sig
   22.16 -  val setup: theory -> theory
   22.17 -  val blacklisted: Proof.context -> thm -> bool
   22.18 -  val add: attribute
   22.19 -  val del: attribute
   22.20 -end;
   22.21 -
   22.22 -structure Res_Blacklist: RES_BLACKLIST =
   22.23 -struct
   22.24 -
   22.25 -structure Data = Generic_Data
   22.26 -(
   22.27 -  type T = thm Termtab.table;
   22.28 -  val empty = Termtab.empty;
   22.29 -  val extend = I;
   22.30 -  fun merge tabs = Termtab.merge (K true) tabs;
   22.31 -);
   22.32 -
   22.33 -fun blacklisted ctxt th =
   22.34 -  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
   22.35 -
   22.36 -fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
   22.37 -fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
   22.38 -
   22.39 -val add = Thm.declaration_attribute add_thm;
   22.40 -val del = Thm.declaration_attribute del_thm;
   22.41 -
   22.42 -val setup =
   22.43 -  Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
   22.44 -  PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
   22.45 -
   22.46 -end;
    23.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 17 19:37:44 2010 +0100
    23.2 +++ b/src/HOL/Wellfounded.thy	Thu Mar 18 12:58:52 2010 +0100
    23.3 @@ -908,7 +908,7 @@
    23.4  lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
    23.5    by (induct n) simp_all
    23.6  
    23.7 -declare "prod.size" [noatp]
    23.8 +declare "prod.size" [no_atp]
    23.9  
   23.10  lemma [code]:
   23.11    "size (P :: 'a Predicate.pred) = 0" by (cases P) simp