src/HOL/Algebra/CRing.thy
changeset 17837 2922be3544f8
parent 16637 62dff56b43d3
child 19233 77ca20b0ed77