src/HOL/Library/Float.thy
changeset 47753 792634c6679e
parent 47621 4cf6011fb884
child 47780 3357688660ff