src/HOL/base.ML
author wenzelm
Tue, 12 Jul 2011 13:45:05 +0200
changeset 43772 c825594fd0c1
parent 37694 19e8b730ddeb
permissions -rw-r--r--
clarified YXML.embed_controls -- this is idempotent and cannot be nested;


(* side-entry for HOL-Base *)

use_thys ["HOL"];