diff -r 3b7477db3462 -r e122cb146ecc Paper/ROOT.ML
--- a/Paper/ROOT.ML	Tue Mar 15 15:53:22 2011 +0000
+++ b/Paper/ROOT.ML	Wed Mar 23 12:17:30 2011 +0000
@@ -1,4 +1,4 @@
 no_document use_thy "../Myhill";
-no_document use_thy "LaTeXsugar";
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
 
 use_thy "Paper"
\ No newline at end of file