src/HOL/main.ML
author haftmann
Thu, 29 Apr 2010 15:00:41 +0200
changeset 36533 f8df589ca2a5
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
permissions -rw-r--r--
dropped unnecessary ML code

(*side-entry for HOL-Main*)
use_thys ["Main"];