src/HOL/main.ML
author haftmann
Thu, 11 Oct 2012 11:56:43 +0200
changeset 49824 c26665a197dc
parent 37694 19e8b730ddeb
permissions -rw-r--r--
msetprod based directly on Multiset.fold; pretty syntax for msetprod_image


(* side-entry for HOL-Main *)

use_thys ["Main"];