src/HOL/Library/Extended_Real.thy
changeset 46978 23a59a495934
parent 45934 9321cd2572fe
child 47082 737d7bc8e50f