# HG changeset patch
# User wenzelm
# Date 1280268202 -7200
# Node ID 3b3187adf2927ee69068bde6913c792bd0ead09a
# Parent  e3ce42cb22dd5c706a558f704275ef5d98d0ee27
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);

diff -r e3ce42cb22dd -r 3b3187adf292 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue Jul 27 23:25:50 2010 +0200
+++ b/src/HOL/Groups.thy	Wed Jul 28 00:03:22 2010 +0200
@@ -6,7 +6,7 @@
 
 theory Groups
 imports Orderings
-uses ("~~/src/HOL/Tools/abel_cancel.ML")
+uses ("Tools/abel_cancel.ML")
 begin
 
 subsection {* Fact collections *}
@@ -802,7 +802,7 @@
 
 end
 
-use "~~/src/HOL/Tools/abel_cancel.ML"
+use "Tools/abel_cancel.ML"
 
 simproc_setup abel_cancel_sum
   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
diff -r e3ce42cb22dd -r 3b3187adf292 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Jul 27 23:25:50 2010 +0200
+++ b/src/HOL/Quotient.thy	Wed Jul 28 00:03:22 2010 +0200
@@ -7,11 +7,11 @@
 theory Quotient
 imports Plain Sledgehammer
 uses
-  ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
-  ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
-  ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
-  ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
-  ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
+  ("Tools/Quotient/quotient_info.ML")
+  ("Tools/Quotient/quotient_typ.ML")
+  ("Tools/Quotient/quotient_def.ML")
+  ("Tools/Quotient/quotient_term.ML")
+  ("Tools/Quotient/quotient_tacs.ML")
 begin
 
 
@@ -708,7 +708,7 @@
 
 text {* Auxiliary data for the quotient package *}
 
-use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
+use "Tools/Quotient/quotient_info.ML"
 
 declare [[map "fun" = (fun_map, fun_rel)]]
 
@@ -728,15 +728,15 @@
   eq_comp_r
 
 text {* Translation functions for the lifting process. *}
-use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
+use "Tools/Quotient/quotient_term.ML"
 
 
 text {* Definitions of the quotient types. *}
-use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
+use "Tools/Quotient/quotient_typ.ML"
 
 
 text {* Definitions for quotient constants. *}
-use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
+use "Tools/Quotient/quotient_def.ML"
 
 
 text {*
@@ -759,7 +759,7 @@
 
 
 text {* Tactics for proving the lifted theorems *}
-use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
+use "Tools/Quotient/quotient_tacs.ML"
 
 subsection {* Methods / Interface *}