src/HOL/Algebra/Algebraic_Closure.thy
changeset 79527 f1f08ca40d96
parent 70215 8371a25ca177
child 80914 d97fdabd9e2b