src/HOL/Algebra/Module.thy
changeset 22885 ebde66a71ab0
parent 20318 0e0ea63fe768
child 27714 27b4d7c01f8b