src/HOL/Quotient.thy
changeset 48891 c0eafbd55de3
parent 47626 f7b1034cb9ce
child 51112 da97167e03f7
     1.1 --- a/src/HOL/Quotient.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -10,12 +10,6 @@
     1.4    "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
     1.5    "quotient_type" :: thy_goal and "/" and
     1.6    "quotient_definition" :: thy_goal
     1.7 -uses
     1.8 -  ("Tools/Quotient/quotient_info.ML")
     1.9 -  ("Tools/Quotient/quotient_type.ML")
    1.10 -  ("Tools/Quotient/quotient_def.ML")
    1.11 -  ("Tools/Quotient/quotient_term.ML")
    1.12 -  ("Tools/Quotient/quotient_tacs.ML")
    1.13  begin
    1.14  
    1.15  text {*
    1.16 @@ -765,7 +759,7 @@
    1.17  
    1.18  text {* Auxiliary data for the quotient package *}
    1.19  
    1.20 -use "Tools/Quotient/quotient_info.ML"
    1.21 +ML_file "Tools/Quotient/quotient_info.ML"
    1.22  setup Quotient_Info.setup
    1.23  
    1.24  declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
    1.25 @@ -787,15 +781,15 @@
    1.26    vimage_id
    1.27  
    1.28  text {* Translation functions for the lifting process. *}
    1.29 -use "Tools/Quotient/quotient_term.ML"
    1.30 +ML_file "Tools/Quotient/quotient_term.ML"
    1.31  
    1.32  
    1.33  text {* Definitions of the quotient types. *}
    1.34 -use "Tools/Quotient/quotient_type.ML"
    1.35 +ML_file "Tools/Quotient/quotient_type.ML"
    1.36  
    1.37  
    1.38  text {* Definitions for quotient constants. *}
    1.39 -use "Tools/Quotient/quotient_def.ML"
    1.40 +ML_file "Tools/Quotient/quotient_def.ML"
    1.41  
    1.42  
    1.43  text {*
    1.44 @@ -820,7 +814,7 @@
    1.45  
    1.46  
    1.47  text {* Tactics for proving the lifted theorems *}
    1.48 -use "Tools/Quotient/quotient_tacs.ML"
    1.49 +ML_file "Tools/Quotient/quotient_tacs.ML"
    1.50  
    1.51  subsection {* Methods / Interface *}
    1.52