src/HOL/Library/Extended_Real.thy
changeset 56019 682bba24e474
parent 55913 c1409c103b77
child 56166 9a241bc276cd