src/HOL/Algebra/Module.thy
changeset 13949 0ce528cd6f19
parent 13940 c67798653056
child 13952 6206d3e7672a
--- a/src/HOL/Algebra/Module.thy	Fri May 02 16:43:36 2003 +0200
+++ b/src/HOL/Algebra/Module.thy	Fri May 02 20:02:50 2003 +0200
@@ -139,7 +139,7 @@
   finally show ?thesis .
 qed
 
-subsection {* Every Abelian Group is a Z-module *}
+subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
 
 text {* Not finished. *}