src/HOL/Library/Float.thy
changeset 42800 df2dc9406287
parent 42676 8724f20bf69c
child 44766 d4d33a4d7548