src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 80383 224cdaaaf0cd
parent 74623 9b1d33c7bbcc
child 80910 406a85a25189