src/HOL/Lattices.thy
changeset 59545 12a6088ed195
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Lattices.thy	Sun Feb 15 08:17:46 2015 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sun Feb 15 17:01:22 2015 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
     1.5      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
     1.6    assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
     1.7 -    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
     1.8 +    and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
     1.9  begin
    1.10  
    1.11  lemma orderI:
    1.12 @@ -53,7 +53,7 @@
    1.13  proof
    1.14    fix a b
    1.15    show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    1.16 -    by (fact semilattice_strict_iff_order)
    1.17 +    by (simp add: order_iff strict_order_iff)
    1.18  next
    1.19    fix a
    1.20    show "a \<preceq> a"