src/HOL/Algebra/Ideal.thy
changeset 29457 2eadbc24de8c
parent 29240 bb81c3709fb6
child 30363 9b8d9b6ef803