src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 41648 6d736d983d5c
parent 41490 0f1e411a1448
child 42616 92715b528e78