# HG changeset patch
# User blanchet
# Date 1268913532 -3600
# Node ID 46cfc4b8112e54b407d167ffc8031a7233b9e155
# Parent  f552152d77473996c8c92207f45a1bd7492d47c5
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -1534,12 +1534,12 @@
   from assms show ?thesis by (simp add: Max_def fold1_belowI)
 qed
 
-lemma Min_ge_iff [simp, noatp]:
+lemma Min_ge_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   using assms by (simp add: Min_def min_max.below_fold1_iff)
 
-lemma Max_le_iff [simp, noatp]:
+lemma Max_le_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
 proof -
@@ -1548,12 +1548,12 @@
   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
 qed
 
-lemma Min_gr_iff [simp, noatp]:
+lemma Min_gr_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   using assms by (simp add: Min_def strict_below_fold1_iff)
 
-lemma Max_less_iff [simp, noatp]:
+lemma Max_less_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
 proof -
@@ -1563,12 +1563,12 @@
     by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
 qed
 
-lemma Min_le_iff [noatp]:
+lemma Min_le_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   using assms by (simp add: Min_def fold1_below_iff)
 
-lemma Max_ge_iff [noatp]:
+lemma Max_ge_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
 proof -
@@ -1578,12 +1578,12 @@
     by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
 qed
 
-lemma Min_less_iff [noatp]:
+lemma Min_less_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   using assms by (simp add: Min_def fold1_strict_below_iff)
 
-lemma Max_gr_iff [noatp]:
+lemma Max_gr_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
 proof -
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -231,7 +231,7 @@
     by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
 qed
 
-lemma Union_iff [simp, noatp]:
+lemma Union_iff [simp, no_atp]:
   "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
   by (unfold Union_eq) blast
 
@@ -269,10 +269,10 @@
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   by blast
 
-lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   by blast
 
-lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   by blast
 
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
@@ -332,7 +332,7 @@
   "\<Union>S = (\<Union>x\<in>S. x)"
   by (simp add: UNION_eq_Union_image image_def)
 
-lemma UNION_def [noatp]:
+lemma UNION_def [no_atp]:
   "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   by (auto simp add: UNION_eq_Union_image Union_eq)
   
@@ -368,13 +368,13 @@
 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (iprover intro: subsetI elim: UN_E dest: subsetD)
 
-lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   by blast
 
 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
-lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
+lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
   by blast
 
 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
@@ -412,7 +412,7 @@
   "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
 by blast+
 
-lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   by blast
 
 lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
@@ -467,7 +467,7 @@
     by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
 qed
 
-lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
+lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
   by (unfold Inter_eq) blast
 
 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
@@ -515,7 +515,7 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
-lemma Inter_UNIV_conv [simp,noatp]:
+lemma Inter_UNIV_conv [simp,no_atp]:
   "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   by blast+
@@ -724,7 +724,7 @@
   "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
   by auto
 
-lemma ball_simps [simp,noatp]:
+lemma ball_simps [simp,no_atp]:
   "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
   "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
   "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
@@ -739,7 +739,7 @@
   "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
   by auto
 
-lemma bex_simps [simp,noatp]:
+lemma bex_simps [simp,no_atp]:
   "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
   "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
   "!!P. (EX x:{}. P x) = False"
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -19,9 +19,9 @@
 context linorder
 begin
 
-lemma less_not_permute[noatp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
+lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
 
-lemma gather_simps[noatp]: 
+lemma gather_simps[no_atp]: 
   shows 
   "(\<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)"
   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)"
@@ -29,61 +29,61 @@
   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
 
 lemma 
-  gather_start[noatp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
+  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)" 
   by simp
 
 text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
-lemma minf_lt[noatp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
-lemma minf_gt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
+lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
+lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma minf_le[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma minf_ge[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
+lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-lemma minf_eq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
 text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
-lemma pinf_gt[noatp]:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
-lemma pinf_lt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
+lemma pinf_gt[no_atp]:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_lt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma pinf_ge[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma pinf_le[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
+lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-lemma pinf_eq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma pinf_neq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma pinf_P[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma pinf_neq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma pinf_P[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-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
-lemma nmi_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+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
+lemma nmi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
   by (auto simp add: le_less)
-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
-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
-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
-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
-lemma  nmi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
-lemma  nmi_conj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
+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
+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
+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
+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
+lemma  nmi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma  nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
   \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
   \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
-lemma  nmi_disj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
+lemma  nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
   \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
   \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
 
-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)
-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
-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
-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
-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
-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
-lemma  npi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
-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>
+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)
+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
+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
+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
+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
+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
+lemma  npi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+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>
   \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
-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>
+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>
   \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
 
-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)"
+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)"
 proof(clarsimp)
   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"
     and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
@@ -96,7 +96,7 @@
   thus "y < t" using tny by (simp add: less_le)
 qed
 
-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)"
+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)"
 proof(clarsimp)
   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" and xu: "x<u"
@@ -109,7 +109,7 @@
   thus "t < y" using tny by (simp add:less_le)
 qed
 
-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)"
+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)"
 proof(clarsimp)
   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" and xu: "x<u"
@@ -122,7 +122,7 @@
   hence "\<not> t < y"  by auto thus "y \<le> t" by (simp add: not_less)
 qed
 
-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)"
+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)"
 proof(clarsimp)
   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" and xu: "x<u"
@@ -134,11 +134,11 @@
     with tU noU have "False" by auto}
   hence "\<not> y<t"  by auto thus "t \<le> y" by (simp add: not_less)
 qed
-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
-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
-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
+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
+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
+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
 
-lemma lin_dense_conj[noatp]:
+lemma lin_dense_conj[no_atp]:
   "\<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
   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
@@ -146,7 +146,7 @@
   \<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)
   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   by blast
-lemma lin_dense_disj[noatp]:
+lemma lin_dense_disj[no_atp]:
   "\<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
   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
@@ -155,11 +155,11 @@
   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
   by blast
 
-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>
+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>
   \<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')"
 by auto
 
-lemma finite_set_intervals[noatp]:
+lemma finite_set_intervals[no_atp]:
   assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   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"
   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"
@@ -191,7 +191,7 @@
   from ainS binS noy ax xb px show ?thesis by blast
 qed
 
-lemma finite_set_intervals2[noatp]:
+lemma finite_set_intervals2[no_atp]:
   assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   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"
   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)"
@@ -215,7 +215,7 @@
   "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
   by (auto dest: dense)
 
-lemma dlo_qe_bnds[noatp]: 
+lemma dlo_qe_bnds[no_atp]: 
   assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   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)"
 proof (simp only: atomize_eq, rule iffI)
@@ -239,7 +239,7 @@
   ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
 qed
 
-lemma dlo_qe_noub[noatp]: 
+lemma dlo_qe_noub[no_atp]: 
   assumes ne: "L \<noteq> {}" and fL: "finite L"
   shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
 proof(simp add: atomize_eq)
@@ -249,7 +249,7 @@
   thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
 qed
 
-lemma dlo_qe_nolb[noatp]: 
+lemma dlo_qe_nolb[no_atp]: 
   assumes ne: "U \<noteq> {}" and fU: "finite U"
   shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
 proof(simp add: atomize_eq)
@@ -259,14 +259,14 @@
   thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
 qed
 
-lemma exists_neq[noatp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
+lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
   using gt_ex[of t] by auto
 
-lemmas dlo_simps[noatp] = order_refl less_irrefl not_less not_le exists_neq 
+lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom[noatp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
-lemma atoms[noatp]:
+lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
     and "TERM (op = :: 'a \<Rightarrow> _)" .
@@ -277,21 +277,21 @@
 end
 
 (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-lemma dnf[noatp]:
+lemma dnf[no_atp]:
   "(P & (Q | R)) = ((P&Q) | (P&R))" 
   "((Q | R) & P) = ((Q&P) | (R&P))"
   by blast+
 
-lemmas weak_dnf_simps[noatp] = simp_thms dnf
+lemmas weak_dnf_simps[no_atp] = simp_thms dnf
 
-lemma nnf_simps[noatp]:
+lemma nnf_simps[no_atp]:
     "(\<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)"
     "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   by blast+
 
-lemma ex_distrib[noatp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
+lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
 
-lemmas dnf_simps[noatp] = weak_dnf_simps nnf_simps ex_distrib
+lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
 
 use "~~/src/HOL/Tools/Qelim/langford.ML"
 method_setup dlo = {*
@@ -316,10 +316,10 @@
 locale linorder_no_ub = linorder_stupid_syntax +
   assumes gt_ex: "\<exists>y. less x y"
 begin
-lemma ge_ex[noatp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
+lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
 
 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
-lemma pinf_conj[noatp]:
+lemma pinf_conj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
@@ -335,7 +335,7 @@
   thus ?thesis by blast
 qed
 
-lemma pinf_disj[noatp]:
+lemma pinf_disj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
@@ -351,7 +351,7 @@
   thus ?thesis by blast
 qed
 
-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"
+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"
 proof-
   from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   from gt_ex obtain x where x: "z \<sqsubset> x" by blast
@@ -365,11 +365,11 @@
 locale linorder_no_lb = linorder_stupid_syntax +
   assumes lt_ex: "\<exists>y. less y x"
 begin
-lemma le_ex[noatp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
+lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
 
 
 text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
-lemma minf_conj[noatp]:
+lemma minf_conj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
@@ -384,7 +384,7 @@
   thus ?thesis by blast
 qed
 
-lemma minf_disj[noatp]:
+lemma minf_disj[no_atp]:
   assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
@@ -399,7 +399,7 @@
   thus ?thesis by blast
 qed
 
-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"
+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"
 proof-
   from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   from lt_ex obtain x where x: "x \<sqsubset> z" by blast
@@ -422,7 +422,7 @@
 context  constr_dense_linorder
 begin
 
-lemma rinf_U[noatp]:
+lemma rinf_U[no_atp]:
   assumes fU: "finite U"
   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
   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
@@ -465,7 +465,7 @@
     ultimately show ?thesis by blast
   qed
 
-theorem fr_eq[noatp]:
+theorem fr_eq[no_atp]:
   assumes fU: "finite U"
   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
    \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
@@ -493,16 +493,16 @@
  ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
 qed
 
-lemmas minf_thms[noatp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
-lemmas pinf_thms[noatp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
+lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
+lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
 
-lemmas nmi_thms[noatp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
-lemmas npi_thms[noatp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
-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
+lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
+lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
+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
 
-lemma ferrack_axiom[noatp]: "constr_dense_linorder less_eq less between"
+lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between"
   by (rule constr_dense_linorder_axioms)
-lemma atoms[noatp]:
+lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
     and "TERM (op = :: 'a \<Rightarrow> _)" .
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Fields.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -65,7 +65,7 @@
    ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
 by (simp add: division_ring_inverse_add mult_ac)
 
-lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]:
+lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
 proof -
   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
@@ -76,7 +76,7 @@
     finally show ?thesis by (simp add: divide_inverse)
 qed
 
-lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
+lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
 by (simp add: mult_commute [of _ c])
 
@@ -90,7 +90,7 @@
 by (simp add: divide_inverse mult_ac)
 
 text {* These are later declared as simp rules. *}
-lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
 
 lemma add_frac_eq:
   assumes "y \<noteq> 0" and "z \<noteq> 0"
@@ -106,27 +106,27 @@
 
 text{*Special Cancellation Simprules for Division*}
 
-lemma nonzero_mult_divide_cancel_right [simp, noatp]:
+lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
   "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
 using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
 
-lemma nonzero_mult_divide_cancel_left [simp, noatp]:
+lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
   "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
 
-lemma nonzero_divide_mult_cancel_right [simp, noatp]:
+lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
 
-lemma nonzero_divide_mult_cancel_left [simp, noatp]:
+lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
   "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
 
-lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]:
+lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
 using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
 
-lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]:
+lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
 
@@ -139,7 +139,7 @@
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
 by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
-lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)"
+lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
 by (simp add: divide_inverse)
 
 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -183,7 +183,7 @@
 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
 by (erule subst, simp)
 
-lemmas field_eq_simps[noatp] = algebra_simps
+lemmas field_eq_simps[no_atp] = algebra_simps
   (* pull / out*)
   add_divide_eq_iff divide_add_eq_iff
   diff_divide_eq_iff divide_diff_eq_iff
@@ -292,18 +292,18 @@
 apply simp_all
 done
 
-lemma divide_divide_eq_right [simp,noatp]:
+lemma divide_divide_eq_right [simp,no_atp]:
   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
 by (simp add: divide_inverse mult_ac)
 
-lemma divide_divide_eq_left [simp,noatp]:
+lemma divide_divide_eq_left [simp,no_atp]:
   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
 by (simp add: divide_inverse mult_assoc)
 
 
 subsubsection{*Special Cancellation Simprules for Division*}
 
-lemma mult_divide_mult_cancel_left_if[simp,noatp]:
+lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
 fixes c :: "'a :: {field,division_by_zero}"
 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
 by (simp add: mult_divide_mult_cancel_left)
@@ -314,7 +314,7 @@
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
 by (simp add: divide_inverse)
 
-lemma divide_minus_right [simp, noatp]:
+lemma divide_minus_right [simp, no_atp]:
   "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
 by (simp add: divide_inverse)
 
@@ -440,7 +440,7 @@
 done
 
 text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,noatp]:
+lemma inverse_less_iff_less [simp,no_atp]:
   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
 
@@ -448,7 +448,7 @@
   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
 by (force simp add: order_le_less less_imp_inverse_less)
 
-lemma inverse_le_iff_le [simp,noatp]:
+lemma inverse_le_iff_le [simp,no_atp]:
  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
 
@@ -482,7 +482,7 @@
 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
 done
 
-lemma inverse_less_iff_less_neg [simp,noatp]:
+lemma inverse_less_iff_less_neg [simp,no_atp]:
   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
 apply (insert inverse_less_iff_less [of "-b" "-a"])
 apply (simp del: inverse_less_iff_less 
@@ -493,7 +493,7 @@
   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
 by (force simp add: order_le_less less_imp_inverse_less_neg)
 
-lemma inverse_le_iff_le_neg [simp,noatp]:
+lemma inverse_le_iff_le_neg [simp,no_atp]:
  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
@@ -665,7 +665,7 @@
 (for inequations). Can be too aggressive and is therefore separate from the
 more benign @{text algebra_simps}. *}
 
-lemmas field_simps[noatp] = field_eq_simps
+lemmas field_simps[no_atp] = field_eq_simps
   (* multiply ineqn *)
   pos_divide_less_eq neg_divide_less_eq
   pos_less_divide_eq neg_less_divide_eq
@@ -677,7 +677,7 @@
 sign_simps} to @{text field_simps} because the former can lead to case
 explosions. *}
 
-lemmas sign_simps[noatp] = group_simps
+lemmas sign_simps[no_atp] = group_simps
   zero_less_mult_iff  mult_less_0_iff
 
 (* Only works once linear arithmetic is installed:
@@ -716,7 +716,7 @@
       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
 by (simp add: divide_inverse mult_le_0_iff)
 
-lemma divide_eq_0_iff [simp,noatp]:
+lemma divide_eq_0_iff [simp,no_atp]:
      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
 by (simp add: divide_inverse)
 
@@ -756,13 +756,13 @@
 
 subsection{*Cancellation Laws for Division*}
 
-lemma divide_cancel_right [simp,noatp]:
+lemma divide_cancel_right [simp,no_atp]:
      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
 apply (cases "c=0", simp)
 apply (simp add: divide_inverse)
 done
 
-lemma divide_cancel_left [simp,noatp]:
+lemma divide_cancel_left [simp,no_atp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
 apply (cases "c=0", simp)
 apply (simp add: divide_inverse)
@@ -772,23 +772,23 @@
 subsection {* Division and the Number One *}
 
 text{*Simplify expressions equated with 1*}
-lemma divide_eq_1_iff [simp,noatp]:
+lemma divide_eq_1_iff [simp,no_atp]:
      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
 apply (cases "b=0", simp)
 apply (simp add: right_inverse_eq)
 done
 
-lemma one_eq_divide_iff [simp,noatp]:
+lemma one_eq_divide_iff [simp,no_atp]:
      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
 by (simp add: eq_commute [of 1])
 
-lemma zero_eq_1_divide_iff [simp,noatp]:
+lemma zero_eq_1_divide_iff [simp,no_atp]:
      "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
 apply (cases "a=0", simp)
 apply (auto simp add: nonzero_eq_divide_eq)
 done
 
-lemma one_divide_eq_0_iff [simp,noatp]:
+lemma one_divide_eq_0_iff [simp,no_atp]:
      "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"
 apply (cases "a=0", simp)
 apply (insert zero_neq_one [THEN not_sym])
@@ -801,10 +801,10 @@
 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
 
-declare zero_less_divide_1_iff [simp,noatp]
-declare divide_less_0_1_iff [simp,noatp]
-declare zero_le_divide_1_iff [simp,noatp]
-declare divide_le_0_1_iff [simp,noatp]
+declare zero_less_divide_1_iff [simp,no_atp]
+declare divide_less_0_1_iff [simp,no_atp]
+declare zero_le_divide_1_iff [simp,no_atp]
+declare divide_le_0_1_iff [simp,no_atp]
 
 
 subsection {* Ordering Rules for Division *}
@@ -853,22 +853,22 @@
 
 text{*Simplify quotients that are compared with the value 1.*}
 
-lemma le_divide_eq_1 [noatp]:
+lemma le_divide_eq_1 [no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
 by (auto simp add: le_divide_eq)
 
-lemma divide_le_eq_1 [noatp]:
+lemma divide_le_eq_1 [no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
 by (auto simp add: divide_le_eq)
 
-lemma less_divide_eq_1 [noatp]:
+lemma less_divide_eq_1 [no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
 by (auto simp add: less_divide_eq)
 
-lemma divide_less_eq_1 [noatp]:
+lemma divide_less_eq_1 [no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
 by (auto simp add: divide_less_eq)
@@ -876,52 +876,52 @@
 
 subsection{*Conditional Simplification Rules: No Case Splits*}
 
-lemma le_divide_eq_1_pos [simp,noatp]:
+lemma le_divide_eq_1_pos [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
 by (auto simp add: le_divide_eq)
 
-lemma le_divide_eq_1_neg [simp,noatp]:
+lemma le_divide_eq_1_neg [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
 by (auto simp add: le_divide_eq)
 
-lemma divide_le_eq_1_pos [simp,noatp]:
+lemma divide_le_eq_1_pos [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
 by (auto simp add: divide_le_eq)
 
-lemma divide_le_eq_1_neg [simp,noatp]:
+lemma divide_le_eq_1_neg [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
 by (auto simp add: divide_le_eq)
 
-lemma less_divide_eq_1_pos [simp,noatp]:
+lemma less_divide_eq_1_pos [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
 by (auto simp add: less_divide_eq)
 
-lemma less_divide_eq_1_neg [simp,noatp]:
+lemma less_divide_eq_1_neg [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
 by (auto simp add: less_divide_eq)
 
-lemma divide_less_eq_1_pos [simp,noatp]:
+lemma divide_less_eq_1_pos [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
 by (auto simp add: divide_less_eq)
 
-lemma divide_less_eq_1_neg [simp,noatp]:
+lemma divide_less_eq_1_neg [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
 by (auto simp add: divide_less_eq)
 
-lemma eq_divide_eq_1 [simp,noatp]:
+lemma eq_divide_eq_1 [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: eq_divide_eq)
 
-lemma divide_eq_eq_1 [simp,noatp]:
+lemma divide_eq_eq_1 [simp,no_atp]:
   fixes a :: "'a :: {linordered_field,division_by_zero}"
   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -524,13 +524,13 @@
 
 end
 
-lemma UNIV_unit [noatp]:
+lemma UNIV_unit [no_atp]:
   "UNIV = {()}" by auto
 
 instance unit :: finite proof
 qed (simp add: UNIV_unit)
 
-lemma UNIV_bool [noatp]:
+lemma UNIV_bool [no_atp]:
   "UNIV = {False, True}" by auto
 
 instance bool :: finite proof
@@ -1779,7 +1779,7 @@
   "card A > 0 \<Longrightarrow> finite A"
   by (rule ccontr) simp
 
-lemma card_0_eq [simp, noatp]:
+lemma card_0_eq [simp, no_atp]:
   "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
   by (auto dest: mk_disjoint_insert)
 
@@ -2109,8 +2109,8 @@
   show False by simp (blast dest: Suc_neq_Zero surjD)
 qed
 
-(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
-lemma infinite_UNIV_char_0[noatp]:
+(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
+lemma infinite_UNIV_char_0[no_atp]:
   "\<not> finite (UNIV::'a::semiring_char_0 set)"
 proof
   assume "finite (UNIV::'a set)"
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Groups.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -437,7 +437,7 @@
 
 (* FIXME: duplicates right_minus_eq from class group_add *)
 (* but only this one is declared as a simp rule. *)
-lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
+lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
 by (simp add: algebra_simps)
 
 end
@@ -772,12 +772,12 @@
 by (simp add: algebra_simps)
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps[noatp] = algebra_simps
+lemmas group_simps[no_atp] = algebra_simps
 
 end
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps[noatp] = algebra_simps
+lemmas group_simps[no_atp] = algebra_simps
 
 class linordered_ab_semigroup_add =
   linorder + ordered_ab_semigroup_add
@@ -1054,7 +1054,7 @@
 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
 by simp
 
-lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
+lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
 proof -
   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   thus ?thesis by simp
@@ -1201,7 +1201,7 @@
 
 subsection {* Tools setup *}
 
-lemma add_mono_thms_linordered_semiring [noatp]:
+lemma add_mono_thms_linordered_semiring [no_atp]:
   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
@@ -1209,7 +1209,7 @@
     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
 by (rule add_mono, clarify+)+
 
-lemma add_mono_thms_linordered_field [noatp]:
+lemma add_mono_thms_linordered_field [no_atp]:
   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
@@ -1220,8 +1220,8 @@
   add_less_le_mono add_le_less_mono add_strict_mono)
 
 text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
+lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
+lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
 
 ML {*
 structure ab_group_add_cancel = Abel_Cancel
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -23,7 +23,6 @@
   "~~/src/Tools/coherent.ML"
   "~~/src/Tools/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
-  "Tools/res_blacklist.ML"
   ("Tools/simpdata.ML")
   "~~/src/Tools/random_word.ML"
   "~~/src/Tools/atomize_elim.ML"
@@ -35,8 +34,6 @@
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
 
-setup Res_Blacklist.setup
-
 
 subsection {* Primitive logic *}
 
@@ -794,6 +791,25 @@
 
 subsection {* Package setup *}
 
+subsubsection {* Sledgehammer setup *}
+
+text {*
+Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
+that are prolific (match too many equality or membership literals) and relate to
+seldom-used facts. Some duplicate other rules.
+*}
+
+ML {*
+structure No_ATPs = Named_Thms
+(
+  val name = "no_atp"
+  val description = "theorems that should be avoided by Sledgehammer"
+)
+*}
+
+setup {* No_ATPs.setup *}
+
+
 subsubsection {* Classical Reasoner setup *}
 
 lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
@@ -1041,7 +1057,7 @@
 lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
 lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
 
-declare All_def [noatp]
+declare All_def [no_atp]
 
 lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
 lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
@@ -1088,7 +1104,7 @@
 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
 by (simplesubst split_if, blast)
 
-lemmas if_splits [noatp] = split_if split_if_asm
+lemmas if_splits [no_atp] = split_if split_if_asm
 
 lemma if_cancel: "(if c then x else x) = x"
 by (simplesubst split_if, blast)
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Int.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -86,7 +86,7 @@
 
 text{*Reduces equality on abstractions to equality on representatives:
   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
-declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
+declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
 
 text{*Case analysis on the representation of an integer as an equivalence
       class of pairs of naturals.*}
@@ -522,7 +522,7 @@
       It is proved here because attribute @{text arith_split} is not available
       in theory @{text Rings}.
       But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split,noatp]:
+lemma abs_split [arith_split,no_atp]:
      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
@@ -1874,16 +1874,16 @@
 
 text{*These are actually for fields, like real: but where else to put them?*}
 
-lemmas zero_less_divide_iff_number_of [simp, noatp] =
+lemmas zero_less_divide_iff_number_of [simp, no_atp] =
   zero_less_divide_iff [of "number_of w", standard]
 
-lemmas divide_less_0_iff_number_of [simp, noatp] =
+lemmas divide_less_0_iff_number_of [simp, no_atp] =
   divide_less_0_iff [of "number_of w", standard]
 
-lemmas zero_le_divide_iff_number_of [simp, noatp] =
+lemmas zero_le_divide_iff_number_of [simp, no_atp] =
   zero_le_divide_iff [of "number_of w", standard]
 
-lemmas divide_le_0_iff_number_of [simp, noatp] =
+lemmas divide_le_0_iff_number_of [simp, no_atp] =
   divide_le_0_iff [of "number_of w", standard]
 
 
@@ -1896,53 +1896,53 @@
 text {*These laws simplify inequalities, moving unary minus from a term
 into the literal.*}
 
-lemmas less_minus_iff_number_of [simp, noatp] =
+lemmas less_minus_iff_number_of [simp, no_atp] =
   less_minus_iff [of "number_of v", standard]
 
-lemmas le_minus_iff_number_of [simp, noatp] =
+lemmas le_minus_iff_number_of [simp, no_atp] =
   le_minus_iff [of "number_of v", standard]
 
-lemmas equation_minus_iff_number_of [simp, noatp] =
+lemmas equation_minus_iff_number_of [simp, no_atp] =
   equation_minus_iff [of "number_of v", standard]
 
-lemmas minus_less_iff_number_of [simp, noatp] =
+lemmas minus_less_iff_number_of [simp, no_atp] =
   minus_less_iff [of _ "number_of v", standard]
 
-lemmas minus_le_iff_number_of [simp, noatp] =
+lemmas minus_le_iff_number_of [simp, no_atp] =
   minus_le_iff [of _ "number_of v", standard]
 
-lemmas minus_equation_iff_number_of [simp, noatp] =
+lemmas minus_equation_iff_number_of [simp, no_atp] =
   minus_equation_iff [of _ "number_of v", standard]
 
 
 text{*To Simplify Inequalities Where One Side is the Constant 1*}
 
-lemma less_minus_iff_1 [simp,noatp]:
+lemma less_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::{linordered_idom,number_ring}"
   shows "(1 < - b) = (b < -1)"
 by auto
 
-lemma le_minus_iff_1 [simp,noatp]:
+lemma le_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::{linordered_idom,number_ring}"
   shows "(1 \<le> - b) = (b \<le> -1)"
 by auto
 
-lemma equation_minus_iff_1 [simp,noatp]:
+lemma equation_minus_iff_1 [simp,no_atp]:
   fixes b::"'b::number_ring"
   shows "(1 = - b) = (b = -1)"
 by (subst equation_minus_iff, auto)
 
-lemma minus_less_iff_1 [simp,noatp]:
+lemma minus_less_iff_1 [simp,no_atp]:
   fixes a::"'b::{linordered_idom,number_ring}"
   shows "(- a < 1) = (-1 < a)"
 by auto
 
-lemma minus_le_iff_1 [simp,noatp]:
+lemma minus_le_iff_1 [simp,no_atp]:
   fixes a::"'b::{linordered_idom,number_ring}"
   shows "(- a \<le> 1) = (-1 \<le> a)"
 by auto
 
-lemma minus_equation_iff_1 [simp,noatp]:
+lemma minus_equation_iff_1 [simp,no_atp]:
   fixes a::"'b::number_ring"
   shows "(- a = 1) = (a = -1)"
 by (subst minus_equation_iff, auto)
@@ -1950,16 +1950,16 @@
 
 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
 
-lemmas mult_less_cancel_left_number_of [simp, noatp] =
+lemmas mult_less_cancel_left_number_of [simp, no_atp] =
   mult_less_cancel_left [of "number_of v", standard]
 
-lemmas mult_less_cancel_right_number_of [simp, noatp] =
+lemmas mult_less_cancel_right_number_of [simp, no_atp] =
   mult_less_cancel_right [of _ "number_of v", standard]
 
-lemmas mult_le_cancel_left_number_of [simp, noatp] =
+lemmas mult_le_cancel_left_number_of [simp, no_atp] =
   mult_le_cancel_left [of "number_of v", standard]
 
-lemmas mult_le_cancel_right_number_of [simp, noatp] =
+lemmas mult_le_cancel_right_number_of [simp, no_atp] =
   mult_le_cancel_right [of _ "number_of v", standard]
 
 
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 18 12:58:52 2010 +0100
@@ -314,7 +314,6 @@
   Tools/Quotient/quotient_term.ML \
   Tools/Quotient/quotient_typ.ML \
   Tools/recdef.ML \
-  Tools/res_blacklist.ML \
   Tools/Sledgehammer/metis_tactics.ML \
   Tools/Sledgehammer/sledgehammer_fact_filter.ML \
   Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -163,16 +163,16 @@
 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
-lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
+lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x"
   by (simp add: pprt_def sup_aci sup_absorb1)
 
-lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
+lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
   by (simp add: nprt_def inf_aci inf_absorb1)
 
-lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
+lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
   by (simp add: pprt_def sup_aci sup_absorb2)
 
-lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
+lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
   by (simp add: nprt_def inf_aci inf_absorb2)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
@@ -197,10 +197,10 @@
 apply (erule sup_0_imp_0)
 done
 
-lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
+lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
 by (rule, erule inf_0_imp_0) simp
 
-lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
+lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
 by (rule, erule sup_0_imp_0) simp
 
 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
@@ -295,10 +295,10 @@
 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
 unfolding le_iff_inf by (simp add: nprt_def inf_commute)
 
-lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
+lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
 unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
 
-lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
+lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
 unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
 
 end
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/List.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -582,7 +582,7 @@
 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
 by (induct xs) auto
 
-lemma append_eq_append_conv [simp, noatp]:
+lemma append_eq_append_conv [simp, no_atp]:
  "length xs = length ys \<or> length us = length vs
  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
 apply (induct xs arbitrary: ys)
@@ -614,7 +614,7 @@
 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
 using append_same_eq [of "[]"] by auto
 
-lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
 by (induct xs) auto
 
 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
@@ -3928,10 +3928,10 @@
   for A :: "'a set"
 where
     Nil [intro!]: "[]: lists A"
-  | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!,noatp]: "x#l : lists A"
-inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
+  | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+
+inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
+inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
 
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
@@ -3966,15 +3966,15 @@
 
 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
 
-lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
 by (rule in_listsp_conv_set [THEN iffD1])
 
-lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
-
-lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
+
+lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
 by (rule in_listsp_conv_set [THEN iffD2])
 
-lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
+lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
 
 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
 by auto
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -320,7 +320,7 @@
    apply auto
   done
 
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
+lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
   apply (rule trans)
   apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   done
@@ -480,7 +480,7 @@
 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   by (simp add: less_Suc_eq)
 
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
   unfolding One_nat_def by (rule less_Suc0)
 
 lemma Suc_mono: "m < n ==> Suc m < Suc n"
@@ -648,7 +648,7 @@
 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
 by (fast intro: not0_implies_Suc)
 
-lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
 using neq0_conv by blast
 
 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
@@ -1279,10 +1279,10 @@
 
 text{*Special cases where either operand is zero*}
 
-lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
 
-lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
 lemma inj_of_nat: "inj of_nat"
@@ -1327,7 +1327,7 @@
 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
   by (rule of_nat_le_iff [of 0, simplified])
 
-lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Orderings.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -293,11 +293,11 @@
   "max x y < z \<longleftrightarrow> x < z \<and> y < z"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
-lemma split_min [noatp]:
+lemma split_min [no_atp]:
   "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
 by (simp add: min_def)
 
-lemma split_max [noatp]:
+lemma split_max [no_atp]:
   "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
 by (simp add: max_def)
 
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Power.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -334,7 +334,7 @@
   "abs ((-a) ^ n) = abs (a ^ n)"
   by (simp add: power_abs)
 
-lemma zero_less_power_abs_iff [simp, noatp]:
+lemma zero_less_power_abs_iff [simp, no_atp]:
   "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
 proof (induct n)
   case 0 show ?case by simp
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -46,7 +46,7 @@
 where
   "() = Abs_unit True"
 
-lemma unit_eq [noatp]: "u = ()"
+lemma unit_eq [no_atp]: "u = ()"
   by (induct u) (simp add: unit_def Unity_def)
 
 text {*
@@ -78,7 +78,7 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
 instantiation unit :: default
@@ -497,7 +497,7 @@
 lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)
 
-lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
+lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   -- {* For use with @{text split} and the Simplifier. *}
   by (insert surj_pair [of p], clarify, simp)
 
@@ -508,7 +508,7 @@
   current goal contains one of those constants.
 *}
 
-lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
+lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
 by (subst split_split, simp)
 
 
@@ -582,10 +582,10 @@
   Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
 *}
 
-lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   by (rule ext) fast
 
 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
@@ -947,11 +947,11 @@
   -- {* Suggested by Pierre Chartier *}
   by blast
 
-lemma split_paired_Ball_Sigma [simp,noatp]:
+lemma split_paired_Ball_Sigma [simp,no_atp]:
     "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   by blast
 
-lemma split_paired_Bex_Sigma [simp,noatp]:
+lemma split_paired_Bex_Sigma [simp,no_atp]:
     "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   by blast
 
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Relation.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -121,7 +121,7 @@
 lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
 by (simp add: Id_on_def)
 
-lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
+lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
 by (rule Id_on_eqI) (rule refl)
 
 lemma Id_onE [elim!]:
@@ -361,7 +361,7 @@
 
 subsection {* Domain *}
 
-declare Domain_def [noatp]
+declare Domain_def [no_atp]
 
 lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
 by (unfold Domain_def) blast
@@ -484,7 +484,7 @@
 
 subsection {* Image of a set under a relation *}
 
-declare Image_def [noatp]
+declare Image_def [no_atp]
 
 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
 by (simp add: Image_def)
@@ -495,7 +495,7 @@
 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
 by (rule Image_iff [THEN trans]) simp
 
-lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
 by (unfold Image_def) blast
 
 lemma ImageE [elim!]:
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Rings.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -127,7 +127,7 @@
   then show ?thesis ..
 qed
 
-lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
+lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
 by (auto intro: dvd_refl elim!: dvdE)
 
 lemma dvd_0_right [iff]: "a dvd 0"
@@ -221,8 +221,8 @@
 by (rule minus_unique) (simp add: right_distrib [symmetric]) 
 
 text{*Extract signs from products*}
-lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
 
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
 by simp
@@ -236,11 +236,11 @@
 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
 by (simp add: left_distrib diff_minus)
 
-lemmas ring_distribs[noatp] =
+lemmas ring_distribs[no_atp] =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
 
 lemma eq_add_iff1:
   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -252,7 +252,7 @@
 
 end
 
-lemmas ring_distribs[noatp] =
+lemmas ring_distribs[no_atp] =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
@@ -319,7 +319,7 @@
 qed
 
 text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp, noatp]:
+lemma mult_cancel_right [simp, no_atp]:
   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(a * c = b * c) = ((a - b) * c = 0)"
@@ -327,7 +327,7 @@
   thus ?thesis by (simp add: disj_commute)
 qed
 
-lemma mult_cancel_left [simp, noatp]:
+lemma mult_cancel_left [simp, no_atp]:
   "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
 proof -
   have "(c * a = c * b) = (c * (a - b) = 0)"
@@ -743,7 +743,7 @@
 subclass ordered_ab_group_add ..
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
 
 lemma less_add_iff1:
   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
@@ -950,7 +950,7 @@
 end
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
 
 lemmas mult_sign_intros =
   mult_nonneg_nonneg mult_nonneg_nonpos
@@ -1099,7 +1099,7 @@
 
 text {* Simprules for comparisons where common factors can be cancelled. *}
 
-lemmas mult_compare_simps[noatp] =
+lemmas mult_compare_simps[no_atp] =
     mult_le_cancel_right mult_le_cancel_left
     mult_le_cancel_right1 mult_le_cancel_right2
     mult_le_cancel_left1 mult_le_cancel_left2
@@ -1180,7 +1180,7 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
-lemmas eq_minus_self_iff[noatp] = equal_neg_zero
+lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
 
 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Set.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -462,7 +462,7 @@
   unfolding mem_def by (erule le_funE, erule le_boolE)
   -- {* Rule in Modus Ponens style. *}
 
-lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   -- {* The same, with reversed premises for use with @{text erule} --
       cf @{text rev_mp}. *}
   by (rule subsetD)
@@ -471,13 +471,13 @@
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
 
-lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   unfolding mem_def by (blast dest: le_funE le_boolE)
 
-lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
-lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
 lemma subset_refl [simp]: "A \<subseteq> A"
@@ -791,11 +791,11 @@
 
 subsubsection {* Singletons, using insert *}
 
-lemma singletonI [intro!,noatp]: "a : {a}"
+lemma singletonI [intro!,no_atp]: "a : {a}"
     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   by (rule insertI1)
 
-lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
+lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
   by blast
 
 lemmas singletonE = singletonD [elim_format]
@@ -806,11 +806,11 @@
 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   by blast
 
-lemma singleton_insert_inj_eq [iff,noatp]:
+lemma singleton_insert_inj_eq [iff,no_atp]:
      "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   by blast
 
-lemma singleton_insert_inj_eq' [iff,noatp]:
+lemma singleton_insert_inj_eq' [iff,no_atp]:
      "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   by blast
 
@@ -837,7 +837,7 @@
 *}
 
 definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
-  image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
+  image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
 
 abbreviation
   range :: "('a => 'b) => 'b set" where -- "of function"
@@ -942,10 +942,10 @@
 
 subsubsection {* The ``proper subset'' relation *}
 
-lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
+lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   by (unfold less_le) blast
 
-lemma psubsetE [elim!,noatp]: 
+lemma psubsetE [elim!,no_atp]: 
     "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   by (unfold less_le) blast
 
@@ -1102,12 +1102,12 @@
 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   by blast
 
-lemma insert_disjoint [simp,noatp]:
+lemma insert_disjoint [simp,no_atp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
   by auto
 
-lemma disjoint_insert [simp,noatp]:
+lemma disjoint_insert [simp,no_atp]:
  "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   by auto
@@ -1139,7 +1139,7 @@
 by blast
 
 
-lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
+lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
   -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
       with its implicit quantifier and conjunction.  Also image enjoys better
       equational properties than does the RHS. *}
@@ -1156,7 +1156,7 @@
 
 text {* \medskip @{text range}. *}
 
-lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
+lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
   by auto
 
 lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
@@ -1213,7 +1213,7 @@
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   by blast
 
-lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   by blast
 
 lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
@@ -1376,7 +1376,7 @@
 lemma Diff_eq: "A - B = A \<inter> (-B)"
   by blast
 
-lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
+lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
   by blast
 
 lemma Diff_cancel [simp]: "A - A = {}"
@@ -1397,7 +1397,7 @@
 lemma Diff_UNIV [simp]: "A - UNIV = {}"
   by blast
 
-lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
+lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
   by blast
 
 lemma Diff_insert: "A - insert a B = A - B - {a}"
@@ -1639,7 +1639,7 @@
   -- {* monotonicity *}
   by blast
 
-lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
 by (blast intro: sym)
 
 lemma image_vimage_subset: "f ` (f -` A) <= A"
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/SetInterval.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -165,19 +165,19 @@
 context ord
 begin
 
-lemma greaterThanLessThan_iff [simp,noatp]:
+lemma greaterThanLessThan_iff [simp,no_atp]:
   "(i : {l<..<u}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
-lemma atLeastLessThan_iff [simp,noatp]:
+lemma atLeastLessThan_iff [simp,no_atp]:
   "(i : {l..<u}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
-lemma greaterThanAtMost_iff [simp,noatp]:
+lemma greaterThanAtMost_iff [simp,no_atp]:
   "(i : {l<..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
-lemma atLeastAtMost_iff [simp,noatp]:
+lemma atLeastAtMost_iff [simp,no_atp]:
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
@@ -844,7 +844,7 @@
 
 subsubsection {* Some Subset Conditions *}
 
-lemma ivl_subset [simp,noatp]:
+lemma ivl_subset [simp,no_atp]:
  "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
 apply(auto simp:linorder_not_le)
 apply(rule ccontr)
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Mar 18 12:58:52 2010 +0100
@@ -412,10 +412,11 @@
 fun name_thm_pairs ctxt =
   let
     val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
-    fun blacklisted (_, th) =
-      run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
+    val blacklist =
+      if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
+    fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
   in
-    filter_out blacklisted
+    filter_out is_blacklisted
       (fold add_single_names singles (fold add_multi_names mults []))
   end;
 
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Mar 18 12:58:52 2010 +0100
@@ -326,7 +326,7 @@
 
 val multi_base_blacklist =
   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
-   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "noatp" *)
+   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "no_atp" *)
 
 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (Long_Name.explode s);
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Tools/res_blacklist.ML
--- a/src/HOL/Tools/res_blacklist.ML	Wed Mar 17 19:37:44 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      HOL/Tools/res_blacklist.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Makarius
-
-Theorems blacklisted to sledgehammer.  These theorems typically
-produce clauses that are prolific (match too many equality or
-membership literals) and relate to seldom-used facts.  Some duplicate
-other rules.
-*)
-
-signature RES_BLACKLIST =
-sig
-  val setup: theory -> theory
-  val blacklisted: Proof.context -> thm -> bool
-  val add: attribute
-  val del: attribute
-end;
-
-structure Res_Blacklist: RES_BLACKLIST =
-struct
-
-structure Data = Generic_Data
-(
-  type T = thm Termtab.table;
-  val empty = Termtab.empty;
-  val extend = I;
-  fun merge tabs = Termtab.merge (K true) tabs;
-);
-
-fun blacklisted ctxt th =
-  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
-
-fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
-fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
-
-val add = Thm.declaration_attribute add_thm;
-val del = Thm.declaration_attribute del_thm;
-
-val setup =
-  Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
-  PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
-
-end;
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -908,7 +908,7 @@
 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
-declare "prod.size" [noatp]
+declare "prod.size" [no_atp]
 
 lemma [code]:
   "size (P :: 'a Predicate.pred) = 0" by (cases P) simp