src/HOL/Hyperreal/Star.thy
changeset 21471 03a5ef1936c5
parent 21404 eb85850d3eb7
child 21850 bf253f7075b4
equal deleted inserted replaced
21470:7c1b59ddcd56 21471:03a5ef1936c5