src/HOL/SMT_Examples/ROOT.ML

renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

quick_and_dirty := true;
use_thys ["SMT_Tests", "SMT_Examples", "SMT_Word_Examples"];