src/HOL/Nonstandard_Analysis/NSComplex.thy
changeset 75841 7c00d5266bf8
parent 73926 5f71c16f0b37
equal deleted inserted replaced
75840:f8c412a45af8 75841:7c00d5266bf8