src/HOL/Hyperreal/HSeries.thy
changeset 16366 6ff17d08c3d5
parent 15543 0024472afce7
child 17298 ad73fb6144cf
equal deleted inserted replaced
16365:838c65dad23a 16366:6ff17d08c3d5