[isabelle] Bool cpo



Hello,
to make set a cpo, its sufficient to make bool a cpo.
If one defines the "â" operator as the "â" operator on booleans,  one obtains a partial order.
instantiation bool :: pobegin  definition less_bool_def: "(op â) = (op â)"instanceby (intro_classes, unfold less_bool_def, safe)end
This induces an order on sets, which corresponds to the  "â" operator. 
lemma less_set_eq: "(op â) = (op â)"
But this lemma is not accepted by giving this error message:
---Type unification failed: No type arity set :: below---
Can you help me?
Many thanks! 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.