src/HOL/main.ML
author wenzelm
Wed, 19 Sep 2012 21:06:35 +0200
changeset 49448 8a232a4e3fd8
parent 37694 19e8b730ddeb
permissions -rw-r--r--
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);


(* side-entry for HOL-Main *)

use_thys ["Main"];