src/HOL/main.ML
author wenzelm
Thu, 15 Mar 2012 09:55:42 +0100
changeset 46939 5b67ac48b384
parent 37694 19e8b730ddeb
permissions -rw-r--r--
allow multiple 'keywords' as in 'fixes'; tuned comments;


(* side-entry for HOL-Main *)

use_thys ["Main"];