src/HOL/Algebra/Multiplicative_Group.thy
changeset 67907 02a14c1cb917
parent 67399 eab6ce8368fa
child 68157 057d5b4ce47e
equal deleted inserted replaced
67906:9cc32b18c785 67907:02a14c1cb917