src/HOL/Real/RealArith0.thy
author paulson
Wed, 10 Dec 2003 16:47:50 +0100
changeset 14289 deb8e1e62002
parent 14288 d149e3cbdb39
permissions -rw-r--r--
combining Real/{RealArith0,real_arith}.ML

theory RealArith0 = RealBin
files "real_arith0.ML":

setup real_arith_setup

end