src/HOL/Library/Float.thy
changeset 47884 21c42b095c84
parent 47780 3357688660ff
child 47937 70375fa2679d