src/HOL/Nominal/Examples/ROOT.ML

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

use_thys ["Nominal_Examples"];

Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];