src/HOL/Library/Float.thy
changeset 47817 5d2d63f4363e
parent 47780 3357688660ff
child 47937 70375fa2679d