diff -r fb201e383f1b -r da575186d492 Nominal/Ex/Exec/ROOT.ML --- a/Nominal/Ex/Exec/ROOT.ML Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -(* quick_and_dirty := true; *) -no_document use_thys ["~~/src/HOL/Library/LaTeXsugar", - "Name_Exec", "Lambda_Exec"]; -use_thys ["Paper"];