src/HOLCF/Up.thy
changeset 19105 3aabd46340e0
parent 18290 5fc309770840
child 25131 2c8caac48ade
equal deleted inserted replaced
19104:7d69b6d7b8f1 19105:3aabd46340e0
     6 *)
     6 *)
     7 
     7 
     8 header {* The type of lifted values *}
     8 header {* The type of lifted values *}
     9 
     9 
    10 theory Up
    10 theory Up
    11 imports Cfun Sum_Type Datatype
    11 imports Cfun
    12 begin
    12 begin
    13 
    13 
    14 defaultsort cpo
    14 defaultsort cpo
    15 
    15 
    16 subsection {* Definition of new type for lifting *}
    16 subsection {* Definition of new type for lifting *}