src/HOL/Library/comm_ring.ML
changeset 33556 cba22e2999d5
parent 32149 ef59550a55d3
child 33494 2b5b0f9e271c