src/HOL/Real/float.ML
changeset 22963 509b1da3cee1
parent 22951 dfafcd6223ad