src/HOL/Algebra/IntRing.thy
changeset 80150 96f60533ec1d
parent 69597 ff784d5a5bfb