src/HOL/base.ML
author blanchet
Mon, 21 May 2012 10:39:32 +0200
changeset 47946 33afcfad3f8d
parent 37694 19e8b730ddeb
permissions -rw-r--r--
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"


(* side-entry for HOL-Base *)

use_thys ["HOL"];