src/HOL/Library/Extended_Real.thy
changeset 56178 2a6f58938573
parent 56166 9a241bc276cd
child 56212 3253aaf73a01
equal deleted inserted replaced
56177:bfa9dfb722de 56178:2a6f58938573