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