src/HOL/Library/comm_ring.ML
changeset 20665 7e54c7cc72a5
parent 20623 6ae83d153dd4
child 20713 823967ef47f1