src/HOL/Rings.thy
changeset 77215 6cc3b131f761
parent 75962 c530cb79ccbc
child 78935 5e788ff7a489