| changeset 35527 | f4282471461d | 
| parent 35469 | 6e59de61d501 | 
| child 35920 | 9ef9a20cfba1 | 
--- a/src/HOLCF/Fixrec.thy Tue Mar 02 17:34:03 2010 -0800 +++ b/src/HOLCF/Fixrec.thy Tue Mar 02 18:16:28 2010 -0800 @@ -6,7 +6,9 @@ theory Fixrec imports Sprod Ssum Up One Tr Fix -uses ("Tools/fixrec.ML") +uses + ("Tools/holcf_library.ML") + ("Tools/fixrec.ML") begin subsection {* Maybe monad type *} @@ -603,6 +605,7 @@ subsection {* Initializing the fixrec package *} +use "Tools/holcf_library.ML" use "Tools/fixrec.ML" setup {* Fixrec.setup *}