src/HOL/main.ML
author hoelzl
Tue, 10 Mar 2009 16:36:22 +0100
changeset 30413 c41afa5607be
parent 29304 5c71a6da989d
child 33615 261abc2e3155
permissions -rw-r--r--
Fixed type error which appeared when Approximation bounds where specified as floating point numbers

(*side-entry for HOL-Main*)
use_thy "Main";