src/HOL/Complex/NSComplexBin.ML
changeset 14386 ad1ffcc90162
parent 14378 69c4d5997669