src/HOL/Real/Float.thy
changeset 23719 ccd9cb15c062
parent 23477 f4b83f03cac9
child 24124 4399175e3014