src/HOL/Quotient.thy
changeset 37986 3b3187adf292
parent 37593 2505feaf2d70
child 38317 cb8e2ac6397b
     1.1 --- a/src/HOL/Quotient.thy	Tue Jul 27 23:25:50 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Jul 28 00:03:22 2010 +0200
     1.3 @@ -7,11 +7,11 @@
     1.4  theory Quotient
     1.5  imports Plain Sledgehammer
     1.6  uses
     1.7 -  ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
     1.8 -  ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
     1.9 -  ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
    1.10 -  ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
    1.11 -  ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
    1.12 +  ("Tools/Quotient/quotient_info.ML")
    1.13 +  ("Tools/Quotient/quotient_typ.ML")
    1.14 +  ("Tools/Quotient/quotient_def.ML")
    1.15 +  ("Tools/Quotient/quotient_term.ML")
    1.16 +  ("Tools/Quotient/quotient_tacs.ML")
    1.17  begin
    1.18  
    1.19  
    1.20 @@ -708,7 +708,7 @@
    1.21  
    1.22  text {* Auxiliary data for the quotient package *}
    1.23  
    1.24 -use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
    1.25 +use "Tools/Quotient/quotient_info.ML"
    1.26  
    1.27  declare [[map "fun" = (fun_map, fun_rel)]]
    1.28  
    1.29 @@ -728,15 +728,15 @@
    1.30    eq_comp_r
    1.31  
    1.32  text {* Translation functions for the lifting process. *}
    1.33 -use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
    1.34 +use "Tools/Quotient/quotient_term.ML"
    1.35  
    1.36  
    1.37  text {* Definitions of the quotient types. *}
    1.38 -use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
    1.39 +use "Tools/Quotient/quotient_typ.ML"
    1.40  
    1.41  
    1.42  text {* Definitions for quotient constants. *}
    1.43 -use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
    1.44 +use "Tools/Quotient/quotient_def.ML"
    1.45  
    1.46  
    1.47  text {*
    1.48 @@ -759,7 +759,7 @@
    1.49  
    1.50  
    1.51  text {* Tactics for proving the lifted theorems *}
    1.52 -use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
    1.53 +use "Tools/Quotient/quotient_tacs.ML"
    1.54  
    1.55  subsection {* Methods / Interface *}
    1.56