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