src/HOL/base.ML
author wenzelm
Mon, 08 Nov 2010 11:28:22 +0100
changeset 40407 2ff10e613689
parent 37694 19e8b730ddeb
permissions -rw-r--r--
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;


(* side-entry for HOL-Base *)

use_thys ["HOL"];