src/HOL/Algebra/Module.thy
changeset 79527 f1f08ca40d96
parent 68596 81086e6f5429
child 80914 d97fdabd9e2b