src/HOL/Extraction/Euclid.thy
changeset 27125 0733f575b51e
parent 25976 11c6811f232c
child 27982 2aaa4a5569a6