src/HOL/Orderings.thy
changeset 35828 46cfc4b8112e
parent 35579 cc9a5a0ab5ea
child 36635 080b755377c0
--- 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)