# HG changeset patch
# User paulson
# Date 1075214973 -3600
# Node ID dd4e0f2c071a8decd291c7dd4b4d66ab26e1e0e6
# Parent  3d4df8c166aebee83b3215d6df2220f62c7889c6
replacing HOL/Real/PRat, PNat by the rational number development
> of Markus Wenzel

diff -r 3d4df8c166ae -r dd4e0f2c071a src/HOL/Real/RealBin.thy