src/HOL/Euclidean_Rings.thy
changeset 78888 95bbf9a576b3
parent 78668 d52934f126d4
child 82310 41f5266e5595