src/HOLCF/Sprod.thy
changeset 15577 e16da3068ad6
parent 15576 efb95d0d01f7
child 15591 50c3384ca6c4
     1.1 --- a/src/HOLCF/Sprod.thy	Fri Mar 04 23:12:36 2005 +0100
     1.2 +++ b/src/HOLCF/Sprod.thy	Fri Mar 04 23:23:47 2005 +0100
     1.3 @@ -8,7 +8,9 @@
     1.4  
     1.5  header {* The type of strict products *}
     1.6  
     1.7 -theory Sprod = Cfun:
     1.8 +theory Sprod
     1.9 +imports Cfun
    1.10 +begin
    1.11  
    1.12  constdefs
    1.13    Spair_Rep     :: "['a,'b] => ['a,'b] => bool"