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