src/HOL/Library/Float.thy
changeset 33209 d36ca3960e33
parent 32960 69916a850301
child 33555 a0a8a40385a2