src/HOL/ROOT.ML
author wenzelm
Mon, 25 Oct 2010 20:24:13 +0200
changeset 40131 7cbebd636e79
parent 37694 19e8b730ddeb
permissions -rw-r--r--
explicitly qualify type Output.output, which is a slightly odd internal feature;


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];