src/HOL/Library/Extended_Real.thy
changeset 44262 355d5438f5fb
parent 44170 510ac30f44c0
child 44520 316256709a8c