src/HOL/Nonstandard_Analysis/NSComplex.thy
changeset 75488 98d24c6516f6
parent 73926 5f71c16f0b37
equal deleted inserted replaced
75487:167660a8f99e 75488:98d24c6516f6