src/HOL/Algebra/ringsimp.ML
changeset 14024 213dcc39358f
parent 13936 d3671b878828
child 14399 dc677b35e54f