src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 80875 2e33897071b6
parent 74623 9b1d33c7bbcc
child 80910 406a85a25189