src/HOL/Library/Product_ord.thy
 changeset 28519 095fe24b48fd parent 27368 9f90ac19e32b child 28562 4e74209f113e
equal inserted replaced
28518:0329689a1127 28519:095fe24b48fd
`    19   prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"`
`    19   prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"`
`    20 `
`    20 `
`    21 instance ..`
`    21 instance ..`
`    22 `
`    22 `
`    23 end`
`    23 end`
`    29 `
`    24 `
`    30 lemma [code func]:`
`    25 lemma [code func]:`
`    31   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"`
`    26   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"`
`    32   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"`
`    27   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"`
`    33   unfolding prod_le_def prod_less_def by simp_all`
`    28   unfolding prod_le_def prod_less_def by simp_all`