src/HOL/Library/Extended_Real.thy
changeset 44271 89f40a5939b2
parent 44170 510ac30f44c0
child 44520 316256709a8c