src/HOL/ROOT.ML
author blanchet
Thu, 16 Sep 2010 11:12:08 +0200
changeset 39452 70a57e40f795
parent 37694 19e8b730ddeb
permissions -rw-r--r--
factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];