src/HOL/Extraction/Euclid.thy
changeset 38147 2b08a96a283e
parent 37598 893dcabf0c04