src/HOL/main.ML
author boehmes
Thu, 25 Aug 2011 11:15:31 +0200
changeset 44489 6cddca146ca0
parent 37694 19e8b730ddeb
permissions -rw-r--r--
avoid variable clashes by properly incrementing indices


(* side-entry for HOL-Main *)

use_thys ["Main"];