src/HOLCF/HOLCF.thy
changeset 19105 3aabd46340e0
parent 17923 18c66ca0c776
child 23152 9497234a2743
equal deleted inserted replaced
19104:7d69b6d7b8f1 19105:3aabd46340e0
     4 
     4 
     5 HOLCF -- a semantic extension of HOL by the LCF logic.
     5 HOLCF -- a semantic extension of HOL by the LCF logic.
     6 *)
     6 *)
     7 
     7 
     8 theory HOLCF
     8 theory HOLCF
     9 imports Sprod Ssum Up Lift Discrete One Tr Domain
     9 imports Sprod Ssum Up Lift Discrete One Tr Domain Main
    10 uses
    10 uses
    11   "holcf_logic.ML"
    11   "holcf_logic.ML"
    12   "cont_consts.ML"
    12   "cont_consts.ML"
    13   "domain/library.ML"
    13   "domain/library.ML"
    14   "domain/syntax.ML"
    14   "domain/syntax.ML"