src/HOL/Algebra/Embedded_Algebras.thy
changeset 69768 7e4966eaf781
parent 69597 ff784d5a5bfb
child 70160 8e9100dcde52