src/HOL/Algebra/Module.thy
changeset 29270 0eade173f77e
parent 29237 e90d9d51106b
child 35849 b5522b51cb1e