src/HOL/plain.ML
author wenzelm
Thu, 16 Feb 2012 16:42:26 +0100
changeset 46503 186f4cab2ba0
parent 37694 19e8b730ddeb
permissions -rw-r--r--
explicit is better than implicit;


(* side-entry for HOL-Plain *)

use_thys ["Plain"];