src/HOLCF/Fixrec.thy
changeset 23152 9497234a2743
parent 19439 27c2e4cd634b
child 25131 2c8caac48ade
     1.1 --- a/src/HOLCF/Fixrec.thy	Thu May 31 13:24:13 2007 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu May 31 14:01:58 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Fixrec
     1.6  imports Sprod Ssum Up One Tr Fix
     1.7 -uses ("fixrec_package.ML")
     1.8 +uses ("Tools/fixrec_package.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Maybe monad type *}
    1.12 @@ -542,7 +542,7 @@
    1.13  
    1.14  subsection {* Initializing the fixrec package *}
    1.15  
    1.16 -use "fixrec_package.ML"
    1.17 +use "Tools/fixrec_package.ML"
    1.18  
    1.19  hide (open) const return bind fail run
    1.20