src/HOL/Proofs/Extraction/Euclid.thy
changeset 47884 21c42b095c84
parent 45170 7dd207fe7b6e
child 51143 0a2371e7ced3