src/HOL/Algebra/Module.thy
changeset 13940 c67798653056
parent 13936 d3671b878828
child 13949 0ce528cd6f19
--- a/src/HOL/Algebra/Module.thy	Wed Apr 30 18:31:38 2003 +0200
+++ b/src/HOL/Algebra/Module.thy	Wed Apr 30 18:32:06 2003 +0200
@@ -139,7 +139,7 @@
   finally show ?thesis .
 qed
 
-subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
+subsection {* Every Abelian Group is a Z-module *}
 
 text {* Not finished. *}