use fixrec_package.ML
authorhuffman
Sat, 04 Jun 2005 02:11:47 +0200
changeset 16229 77cae9c8e73e
parent 16228 9b5b0c92230a
child 16230 9c9d9ba41bac
use fixrec_package.ML
src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Jun 04 02:11:20 2005 +0200
+++ b/src/HOLCF/Fixrec.thy	Sat Jun 04 02:11:47 2005 +0200
@@ -7,7 +7,7 @@
 
 theory Fixrec
 imports Ssum One Up Fix
-(* files ("fixrec_package.ML") *)
+files ("fixrec_package.ML")
 begin
 
 subsection {* Maybe monad type *}
@@ -137,6 +137,6 @@
 
 subsection {* Intitializing the fixrec package *}
 
-(* use "fixrec_package.ML" *)
+use "fixrec_package.ML"
 
 end