src/HOLCF/Discrete.thy
changeset 19105 3aabd46340e0
parent 16213 88ddef269510
child 25131 2c8caac48ade
equal deleted inserted replaced
19104:7d69b6d7b8f1 19105:3aabd46340e0
     6 *)
     6 *)
     7 
     7 
     8 header {* Discrete cpo types *}
     8 header {* Discrete cpo types *}
     9 
     9 
    10 theory Discrete
    10 theory Discrete
    11 imports Cont Datatype
    11 imports Cont
    12 begin
    12 begin
    13 
    13 
    14 datatype 'a discr = Discr "'a :: type"
    14 datatype 'a discr = Discr "'a :: type"
    15 
    15 
    16 subsection {* Type @{typ "'a discr"} is a partial order *}
    16 subsection {* Type @{typ "'a discr"} is a partial order *}