src/HOL/Library/Extended_Real.thy
changeset 46507 1b24c24017dd
parent 45934 9321cd2572fe
child 47082 737d7bc8e50f
equal deleted inserted replaced
46506:c7faa011bfa7 46507:1b24c24017dd