src/HOL/Rings.thy
changeset 76207 8fcbce9f317c
parent 75962 c530cb79ccbc
child 78935 5e788ff7a489