src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 80182 29f2b8ff84f3
parent 74623 9b1d33c7bbcc
child 80910 406a85a25189