src/HOLCF/domain/extender.ML
changeset 2446 c2a9bf6c0948
parent 2445 51993fea433f
child 4008 2444085532c6
equal deleted inserted replaced
2445:51993fea433f 2446:c2a9bf6c0948
     3     Author : David von Oheimb
     3     Author : David von Oheimb
     4     Copyright 1995, 1996 TU Muenchen
     4     Copyright 1995, 1996 TU Muenchen
     5 
     5 
     6 theory extender for domain section
     6 theory extender for domain section
     7 *)
     7 *)
       
     8 
     8 
     9 
     9 structure Domain_Extender =
    10 structure Domain_Extender =
    10 struct
    11 struct
    11 
    12 
    12 local
    13 local