src/HOL/Nominal/Examples/ROOT.ML
changeset 28392 d10839c203bd
parent 27623 8e9c19529a4e
child 28654 2f9857126498
equal deleted inserted replaced
28391:1a4804fc2216 28392:d10839c203bd
    21   "Support",
    21   "Support",
    22   "Contexts",
    22   "Contexts",
    23   "Standardization"
    23   "Standardization"
    24 ];
    24 ];
    25 
    25 
    26 setmp quick_and_dirty true use_thy "VC_Condition";
    26 setmp_noncritical quick_and_dirty true use_thy "VC_Condition";