src/HOL/Algebra/CRing.thy
changeset 17517 9dc9d3005ed2
parent 16637 62dff56b43d3
child 19233 77ca20b0ed77