src/HOL/Hyperreal/HyperArith0.thy
author wenzelm
Fri, 09 Nov 2001 22:52:38 +0100
changeset 12130 30d9143aff7e
parent 10751 a81ea5d3dd41
permissions -rw-r--r--
syntactic declaration of external *and* internal versions of fixes; tuned warn_extra_tfrees;

theory HyperArith0 = HyperBin
files "hypreal_arith0.ML":

setup hypreal_arith_setup

end