src/HOL/main.ML
author ballarin
Thu, 06 Jan 2011 21:06:17 +0100
changeset 41433 1b8ff770f02c
parent 37694 19e8b730ddeb
permissions -rw-r--r--
Abelian group facts obtained from group facts via interpretation (sublocale).


(* side-entry for HOL-Main *)

use_thys ["Main"];