src/HOL/Library/Extended_Real.thy
changeset 44591 0b107d11f634
parent 44520 316256709a8c
child 44669 8e6cdb9c00a7