src/HOL/Nominal/Examples/ROOT.ML

fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"

use_thys ["Nominal_Examples"];

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