src/HOL/Algebra/Module.thy
changeset 14722 8e739a6eaf11
parent 14706 71590b7733b7
child 15095 63f5f4c265dd