src/HOL/Library/comm_ring.ML
changeset 27263 a6b7f934fbc4
parent 26939 1035c89b4c02
child 29265 5b4247055bd7