new file float_syntax.ML
authornipkow
Sat Nov 29 13:39:23 2008 +0100 (2008-11-29)
changeset 28905c999579a5166
parent 28904 3ef9489eeef5
child 28906 5f568bfc58d7
new file float_syntax.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Sat Nov 29 13:37:13 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Nov 29 13:39:23 2008 +0100
     1.3 @@ -272,6 +272,7 @@
     1.4    Library/Parity.thy \
     1.5    Library/Univ_Poly.thy \
     1.6    Real/ContNotDenum.thy \
     1.7 +  Real/float_syntax.ML \
     1.8    Real/Lubs.thy \
     1.9    Real/PReal.thy \
    1.10    Real/rat_arith.ML \