src/HOL/Algebra/Ideal.thy
changeset 74370 d8dc8fdc46fc
parent 70215 8371a25ca177
child 80914 d97fdabd9e2b