src/HOL/main.ML
author wenzelm
Fri, 08 Jul 2011 15:17:40 +0200
changeset 43703 c37a1f29bbc0
parent 37694 19e8b730ddeb
permissions -rw-r--r--
standardized String.concat towards implode;


(* side-entry for HOL-Main *)

use_thys ["Main"];