src/HOLCF/Domain.thy
changeset 16223 84a177eeb49c
parent 16217 96f0c8546265
child 16230 9c9d9ba41bac
     1.1 --- a/src/HOLCF/Domain.thy	Sat Jun 04 00:22:22 2005 +0200
     1.2 +++ b/src/HOLCF/Domain.thy	Sat Jun 04 00:23:40 2005 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  header {* Domain package *}
     1.5  
     1.6  theory Domain
     1.7 -imports Ssum Sprod One Up
     1.8 +imports Ssum Sprod One Up Fixrec
     1.9 +(*
    1.10  files
    1.11    ("domain/library.ML")
    1.12    ("domain/syntax.ML")
    1.13 @@ -14,6 +15,7 @@
    1.14    ("domain/theorems.ML")
    1.15    ("domain/extender.ML")
    1.16    ("domain/interface.ML")
    1.17 +*)
    1.18  begin
    1.19  
    1.20  defaultsort pcpo