src/HOL/Library/sum_of_squares.ML
changeset 31327 ffa5356cc343
parent 31131 d9752181691a
child 31512 27118561c2e0