src/HOL/Orderings.thy
changeset 24286 7619080e49f0
parent 23948 261bd4678076
child 24422 c0b5ff9e9e4d
     1.1 --- a/src/HOL/Orderings.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -225,11 +225,11 @@
     1.4    "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
     1.5  unfolding max_def le_less using less_linear by (auto intro: less_trans)
     1.6  
     1.7 -lemma split_min:
     1.8 +lemma split_min [noatp]:
     1.9    "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
    1.10  by (simp add: min_def)
    1.11  
    1.12 -lemma split_max:
    1.13 +lemma split_max [noatp]:
    1.14    "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
    1.15  by (simp add: max_def)
    1.16