src/HOL/Complex/NSInduct.thy
changeset 14470 1ffe42cfaefe
parent 14469 c7674b7034f5