src/HOLCF/Fixrec.thy
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 *}