src/HOL/Library/Extended_Real.thy
changeset 70490 c42a0a0a9a8d
parent 70367 81b65ddac59f
child 70532 fcf3b891ccb1