src/HOL/ex/Pythagoras.thy
changeset 66542 075bbb78d33c
parent 62390 842917225d56