src/HOL/SMT_Examples/ROOT.ML
author blanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 43188 0c36ae874fcc
parent 36900 631e961a9e95
permissions -rw-r--r--
fixed detection of Skolem constants in type construction detection code

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