# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1324152217 0
# Node ID 31d51ce547b78f742b68a712268492c7e79b2c92
# Parent  da60dc911055049d73a6801c1cde48bb772dcef5
updated

diff -r da60dc911055 -r 31d51ce547b7 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Fri Dec 16 16:01:12 2011 +0900
+++ b/Nominal/ROOT.ML	Sat Dec 17 20:03:37 2011 +0000
@@ -32,8 +32,6 @@
 quick_and_dirty := true;
 
 no_document use_thys
-   ["Ex/Classical",    
-    "Ex/Let"
-   ];
+   ["Ex/Let"];