src/HOL/Hyperreal/Lim.thy
changeset 15827 5fdf2d8dab9c
parent 15539 333a88244569
child 16924 04246269386e
equal deleted inserted replaced
15826:e9b4c9feb296 15827:5fdf2d8dab9c