src/HOL/Rings.thy
changeset 77830 0f2baf04b782
parent 75962 c530cb79ccbc
child 78935 5e788ff7a489