src/HOL/ex/Pythagoras.thy
changeset 59859 f9d1442c70f3
parent 59190 3a594fd13ca4
child 61343 5b5656a63bd6