src/HOL/Library/Float.thy
changeset 69457 bea49e443909
parent 69064 5840724b1d71
child 69593 3dda49e08b9d