src/HOL/Library/Float.thy
changeset 41255 a80024d7b71b
parent 41024 ba961a606c67
child 41528 276078f01ada