src/HOL/SMT_Examples/ROOT.ML
author blanchet
Wed, 21 Jul 2010 21:16:58 +0200
changeset 37928 24785fa2416c
parent 36900 631e961a9e95
permissions -rw-r--r--
do a better job at Skolemizing in Nitpick, for TPTP FOF

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