removed fixme - quick-and-dirty flag is appropriate
authorChristian Urban <urbanc@in.tum.de>
Fri, 20 Nov 2009 00:54:20 +0100
changeset 33773 ccef2e6d8c21
parent 33772 b6a1feca2ac2
child 33803 f5db63bd7aee
removed fixme - quick-and-dirty flag is appropriate
src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Nov 20 00:20:32 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Nov 20 00:54:20 2009 +0100
@@ -1,3 +1,3 @@
 use_thys ["Nominal_Examples"];
 
-setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];