src/HOL/Extraction/Euclid.thy
changeset 31291 a2f737a72655
parent 30047 46c88406e6c0
child 31953 eeb8a300f362
equal deleted inserted replaced
31290:f41c023d90bc 31291:a2f737a72655