src/HOL/base.ML
author krauss
Sun, 01 Apr 2012 22:03:45 +0200
changeset 47259 2d4ea84278da
parent 37694 19e8b730ddeb
permissions -rw-r--r--
removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare


(* side-entry for HOL-Base *)

use_thys ["HOL"];