src/HOLCF/Porder.thy
changeset 19105 3aabd46340e0
parent 18647 5f5d37e763c4
child 19621 475140eb82f2
equal deleted inserted replaced
19104:7d69b6d7b8f1 19105:3aabd46340e0
     4 *)
     4 *)
     5 
     5 
     6 header {* Partial orders *}
     6 header {* Partial orders *}
     7 
     7 
     8 theory Porder
     8 theory Porder
     9 imports Main
     9 imports Datatype
    10 begin
    10 begin
    11 
    11 
    12 subsection {* Type class for partial orders *}
    12 subsection {* Type class for partial orders *}
    13 
    13 
    14 	-- {* introduce a (syntactic) class for the constant @{text "<<"} *}
    14 	-- {* introduce a (syntactic) class for the constant @{text "<<"} *}