src/HOL/ex/Pythagoras.thy
changeset 59614 452458cf8506
parent 59190 3a594fd13ca4
child 61343 5b5656a63bd6