src/HOL/HOLCF/Domain_Aux.thy
changeset 48891 c0eafbd55de3
parent 42151 4da4fc77664b
child 56511 265816f87386
     1.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,12 +6,6 @@
     1.4  
     1.5  theory Domain_Aux
     1.6  imports Map_Functions Fixrec
     1.7 -uses
     1.8 -  ("Tools/Domain/domain_take_proofs.ML")
     1.9 -  ("Tools/cont_consts.ML")
    1.10 -  ("Tools/cont_proc.ML")
    1.11 -  ("Tools/Domain/domain_constructors.ML")
    1.12 -  ("Tools/Domain/domain_induction.ML")
    1.13  begin
    1.14  
    1.15  subsection {* Continuous isomorphisms *}
    1.16 @@ -350,11 +344,11 @@
    1.17  
    1.18  subsection {* ML setup *}
    1.19  
    1.20 -use "Tools/Domain/domain_take_proofs.ML"
    1.21 -use "Tools/cont_consts.ML"
    1.22 -use "Tools/cont_proc.ML"
    1.23 -use "Tools/Domain/domain_constructors.ML"
    1.24 -use "Tools/Domain/domain_induction.ML"
    1.25 +ML_file "Tools/Domain/domain_take_proofs.ML"
    1.26 +ML_file "Tools/cont_consts.ML"
    1.27 +ML_file "Tools/cont_proc.ML"
    1.28 +ML_file "Tools/Domain/domain_constructors.ML"
    1.29 +ML_file "Tools/Domain/domain_induction.ML"
    1.30  
    1.31  setup Domain_Take_Proofs.setup
    1.32