src/HOL/Library/Float.thy
changeset 59488 8a183caa424d
parent 59487 adaa430fc0f7
child 59554 4044f53326c9