src/HOL/Proofs/Extraction/Euclid.thy
changeset 48973 fcd21f714996
parent 45170 7dd207fe7b6e
child 51143 0a2371e7ced3