src/HOL/HOLCF/Fixrec.thy
changeset 48891 c0eafbd55de3
parent 47432 e1576d13e933
child 49759 ecf1d5d87e5e
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,9 +7,6 @@
     1.4  theory Fixrec
     1.5  imports Plain_HOLCF
     1.6  keywords "fixrec" :: thy_decl
     1.7 -uses
     1.8 -  ("Tools/holcf_library.ML")
     1.9 -  ("Tools/fixrec.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Pattern-match monad *}
    1.13 @@ -227,8 +224,8 @@
    1.14  
    1.15  subsection {* Initializing the fixrec package *}
    1.16  
    1.17 -use "Tools/holcf_library.ML"
    1.18 -use "Tools/fixrec.ML"
    1.19 +ML_file "Tools/holcf_library.ML"
    1.20 +ML_file "Tools/fixrec.ML"
    1.21  
    1.22  method_setup fixrec_simp = {*
    1.23    Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)