src/HOL/Extraction/Euclid.thy
changeset 30242 aea5d7fa7ef5
parent 30047 46c88406e6c0
child 31953 eeb8a300f362