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 -