src/HOL/Library/Extended_Real.thy
changeset 46454 d72ab6bf6e6d
parent 45934 9321cd2572fe
child 47082 737d7bc8e50f