--- a/Paper/ROOT.ML	Tue May 31 20:32:49 2011 +0000
+++ b/Paper/ROOT.ML	Thu Jun 02 16:44:35 2011 +0000
@@ -1,4 +1,3 @@
 no_document use_thy "../Myhill";
-no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
 
 use_thy "Paper"
\ No newline at end of file