1.1 --- a/src/HOL/Orderings.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -293,11 +293,11 @@
     1.4    "max x y < z \<longleftrightarrow> x < z \<and> y < z"
     1.5  unfolding max_def le_less using less_linear by (auto intro: less_trans)
     1.6  
     1.7 -lemma split_min [noatp]:
     1.8 +lemma split_min [no_atp]:
     1.9    "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
    1.10  by (simp add: min_def)
    1.11  
    1.12 -lemma split_max [noatp]:
    1.13 +lemma split_max [no_atp]:
    1.14    "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
    1.15  by (simp add: max_def)
    1.16