# HG changeset patch # User berghofe # Date 1224616846 -7200 # Node ID 2f98571264983ae2098ce08647f8d9b67605d38f # Parent 4593c70e228eeffa15409ff12bc32b6eaa191c98 Added theory W. diff -r 4593c70e228e -r 2f9857126498 src/HOL/Nominal/Examples/ROOT.ML --- a/src/HOL/Nominal/Examples/ROOT.ML Tue Oct 21 21:20:17 2008 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Tue Oct 21 21:20:46 2008 +0200 @@ -20,7 +20,8 @@ "LocalWeakening", "Support", "Contexts", - "Standardization" + "Standardization", + "W" ]; setmp_noncritical quick_and_dirty true use_thy "VC_Condition";