src/HOL/Library/Sum_of_Squares.thy
changeset 82233 3e972fc58373
parent 70333 0f7edf0853df