src/HOL/Library/Float.thy
changeset 73630 f2e836e013cb
parent 72607 feebdaa346e5
child 73655 26a1d66b9077