src/HOL/Hyperreal/HyperDef.thy
changeset 26964 df1f238a05f7
parent 26566 36a93808642c
child 27105 5f139027c365
equal deleted inserted replaced
26963:290d23780204 26964:df1f238a05f7