src/HOL/Proofs/Extraction/Euclid.thy
changeset 63045 c50c764aab10
parent 61986 2461779da2b8
child 63361 d10eab0672f9