src/HOL/Library/sum_of_squares.ML
changeset 32331 e60684ecaf3d
parent 32268 d50f0cb67578