src/HOL/Euclidean_Rings.thy
changeset 82407 fcc0f74ac086
parent 82310 41f5266e5595
child 82518 da14e77a48b2