src/HOL/Algebra/Ideal.thy
changeset 77820 15edec78869c
parent 70215 8371a25ca177
child 80914 d97fdabd9e2b