src/HOL/base.ML
author bulwahn
Sat, 09 Jul 2011 21:09:09 +0200
changeset 43735 9b88fd07b912
parent 37694 19e8b730ddeb
permissions -rw-r--r--
standardized String.concat towards implode (cf. c37a1f29bbc0)


(* side-entry for HOL-Base *)

use_thys ["HOL"];