use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
authorwenzelm
Wed Jul 28 00:03:22 2010 +0200 (2010-07-28)
changeset 379863b3187adf292
parent 37985 e3ce42cb22dd
child 37987 aac4eb1fa1d8
use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
src/HOL/Groups.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Groups.thy	Tue Jul 27 23:25:50 2010 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed Jul 28 00:03:22 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Groups
     1.6  imports Orderings
     1.7 -uses ("~~/src/HOL/Tools/abel_cancel.ML")
     1.8 +uses ("Tools/abel_cancel.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Fact collections *}
    1.12 @@ -802,7 +802,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -use "~~/src/HOL/Tools/abel_cancel.ML"
    1.17 +use "Tools/abel_cancel.ML"
    1.18  
    1.19  simproc_setup abel_cancel_sum
    1.20    ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
     2.1 --- a/src/HOL/Quotient.thy	Tue Jul 27 23:25:50 2010 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Wed Jul 28 00:03:22 2010 +0200
     2.3 @@ -7,11 +7,11 @@
     2.4  theory Quotient
     2.5  imports Plain Sledgehammer
     2.6  uses
     2.7 -  ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
     2.8 -  ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
     2.9 -  ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
    2.10 -  ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
    2.11 -  ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
    2.12 +  ("Tools/Quotient/quotient_info.ML")
    2.13 +  ("Tools/Quotient/quotient_typ.ML")
    2.14 +  ("Tools/Quotient/quotient_def.ML")
    2.15 +  ("Tools/Quotient/quotient_term.ML")
    2.16 +  ("Tools/Quotient/quotient_tacs.ML")
    2.17  begin
    2.18  
    2.19  
    2.20 @@ -708,7 +708,7 @@
    2.21  
    2.22  text {* Auxiliary data for the quotient package *}
    2.23  
    2.24 -use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
    2.25 +use "Tools/Quotient/quotient_info.ML"
    2.26  
    2.27  declare [[map "fun" = (fun_map, fun_rel)]]
    2.28  
    2.29 @@ -728,15 +728,15 @@
    2.30    eq_comp_r
    2.31  
    2.32  text {* Translation functions for the lifting process. *}
    2.33 -use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
    2.34 +use "Tools/Quotient/quotient_term.ML"
    2.35  
    2.36  
    2.37  text {* Definitions of the quotient types. *}
    2.38 -use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
    2.39 +use "Tools/Quotient/quotient_typ.ML"
    2.40  
    2.41  
    2.42  text {* Definitions for quotient constants. *}
    2.43 -use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
    2.44 +use "Tools/Quotient/quotient_def.ML"
    2.45  
    2.46  
    2.47  text {*
    2.48 @@ -759,7 +759,7 @@
    2.49  
    2.50  
    2.51  text {* Tactics for proving the lifted theorems *}
    2.52 -use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
    2.53 +use "Tools/Quotient/quotient_tacs.ML"
    2.54  
    2.55  subsection {* Methods / Interface *}
    2.56