src/HOL/Extraction/Euclid.thy
changeset 31106 9a1178204dc0
parent 30047 46c88406e6c0
child 31953 eeb8a300f362