src/HOL/Library/Extended_Real.thy
changeset 64722 6df73de0d3c7
parent 64272 f76b6dda2e56
child 65680 378a2f11bec9