src/HOL/Real/Float.thy
changeset 23961 9e7e1e309ebd
parent 23477 f4b83f03cac9
child 24124 4399175e3014
equal deleted inserted replaced
23960:c07ae96cbfc4 23961:9e7e1e309ebd