src/HOL/Library/Float.thy
changeset 79834 45b81ff3c972
parent 79560 5c2c8a60b77e
child 80452 0303b3a0edde