src/HOL/ROOT.ML
author Brian Huffman <brianh@cs.pdx.edu>
Tue, 05 Oct 2010 17:07:57 -0700
changeset 39970 9023b897e67a
parent 37694 19e8b730ddeb
permissions -rw-r--r--
simplify proofs of powerdomain inequalities


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];