src/HOL/Nominal/Examples/ROOT.ML

use orig_text_painter for extras outside main text (also required to update internal line infos);
tuned;

use_thys ["Nominal_Examples"];

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