src/HOL/Algebra/IntRing.thy
changeset 29270 0eade173f77e
parent 29242 e190bc2a5399
child 29424 948d616959e4