src/HOL/Library/Float.thy
changeset 44656 22bbd0d1b943
parent 42676 8724f20bf69c
child 44766 d4d33a4d7548