src/HOL/Extraction/Euclid.thy
changeset 25446 c1be3072ea8f
parent 25422 37e991068d96
child 25687 f92c9dfa7681