| changeset 33773 | ccef2e6d8c21 |
| parent 33615 | 261abc2e3155 |
| child 39616 | 8052101883c3 |
--- 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"];