src/HOL/Algebra/CRing.thy
changeset 15401 ba28d103bada
parent 15328 35951e6a7855
child 15696 1da4ce092c0b