src/HOL/ROOT.ML
author blanchet
Thu, 16 Dec 2010 22:43:22 +0100
changeset 41219 41f3fdc49ec3
parent 37694 19e8b730ddeb
permissions -rw-r--r--
keep track of errors in Z3 input file for debugging purposes


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];