src/HOL/Complex/NSComplex.thy
changeset 23563 42f2f90b51a6
parent 23126 93f8cb025afd
child 27148 5b78e50adc49