src/HOL/main.ML
author haftmann
Sat, 24 Jul 2010 18:08:41 +0200
changeset 37958 9728342bcd56
parent 37694 19e8b730ddeb
permissions -rw-r--r--
another refinement chapter in the neverending numeral story


(* side-entry for HOL-Main *)

use_thys ["Main"];