src/HOL/Library/Float.thy
changeset 80182 29f2b8ff84f3
parent 79560 5c2c8a60b77e
child 80452 0303b3a0edde