src/HOL/Library/comm_ring.ML
changeset 20335 b5eca86ef9cc
parent 19233 77ca20b0ed77
child 20623 6ae83d153dd4