src/HOL/SMT_Examples/ROOT.ML

adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck

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