src/HOL/ex/Pythagoras.thy
changeset 81512 c1aa8a61ee65
parent 62390 842917225d56