src/HOL/Euclidean_Rings.thy
changeset 78515 c9fb5e7975c5
parent 77812 fb3d81bd9803
child 78668 d52934f126d4