--- a/Fun-Paper/ROOT.ML Sat Dec 17 16:58:11 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; - -use_thy "Paper" \ No newline at end of file