src/HOL/Library/Float.thy
changeset 80459 00fcbb277dae
parent 79560 5c2c8a60b77e
child 80452 0303b3a0edde