src/HOL/ex/Pythagoras.thy
changeset 60307 75e1aa7a450e
parent 59190 3a594fd13ca4
child 61343 5b5656a63bd6