src/HOL/Complex/NSInduct.thy
changeset 14418 b62323c85134
parent 14409 91181ee5860c
child 14469 c7674b7034f5