src/HOL/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Tue, 11 May 2010 07:45:47 +0100
changeset 36812 e090bdb4e1c5
parent 34205 f69cd974bc4e
child 37694 19e8b730ddeb
permissions -rw-r--r--
tuned proof so that no simplifier warning is printed

(* Classical Higher-order Logic -- batteries included *)

use_thys ["Complex_Main"];