src/HOL/Complex/NSInduct.thy
changeset 14415 60aa114e2dba
parent 14409 91181ee5860c
child 14469 c7674b7034f5