src/HOL/Library/Extended_Real.thy
changeset 61218 04c769fe1cb5
parent 61188 b34551d94934
child 61245 b77bf45efe21