src/HOLCF/Fixrec.thy
changeset 16229 77cae9c8e73e
parent 16221 879400e029bf
child 16401 57c35ede00b9
--- 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