src/HOL/Complex/NSInduct.ML
changeset 14182 5f49f00fe084
parent 13957 10dbf16be15f
child 14371 c78c7da09519