src/HOL/Complete_Partial_Order.thy
changeset 60057 86fa63ce8156
parent 58889 5b7a9633cfa8
child 60061 279472fa0b1d
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -53,6 +53,9 @@
     1.4  lemma chain_empty: "chain ord {}"
     1.5  by(simp add: chain_def)
     1.6  
     1.7 +lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
     1.8 +by(auto simp add: chain_def)
     1.9 +
    1.10  subsection {* Chain-complete partial orders *}
    1.11  
    1.12  text {*