src/HOL/Library/comm_ring.ML
changeset 22949 997cef733bdd
parent 21588 cd0dc678a205
child 22950 8b6d28fc6532