doc-src/IsarRef/Thy/ROOT-ZF.ML
author blanchet
Mon, 08 Nov 2010 02:33:48 +0100
changeset 40419 718b44dbd74d
parent 38767 d8da44a8dd25
child 42651 e3fdb7c96be5
permissions -rw-r--r--
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice

Thy_Output.source_default := true;
use "../../antiquote_setup.ML";

use_thy "ZF_Specific";