src/HOL/Library/Extended_Real.thy
changeset 46471 2289a3869c88
parent 45934 9321cd2572fe
child 47082 737d7bc8e50f