src/HOL/Algebra/Module.thy
changeset 16877 e92cba1d4842
parent 16417 9bc16273c2d4
child 19783 82f365a14960