src/HOL/Library/comm_ring.ML
changeset 30890 0214d179c2be
parent 30510 4120fc59dd85
child 31021 53642251a04f