--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/ROOT.ML	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,4 @@
+(* quick_and_dirty := true; *)
+no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
+                      "Name_Exec", "Lambda_Exec"];
+use_thys ["Paper"];