# HG changeset patch
# User ballarin
# Date 1052124807 -7200
# Node ID 6206d3e7672aabd6f5c159648f7b56ae9c53148f
# Parent  e2bf2551eb9ae14f6c62f85b5806521979cdc90b
Fixed but with old versions of pdflatex (fancy symbols not allowed in bookmarks).

diff -r e2bf2551eb9a -r 6206d3e7672a src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sat May 03 13:31:07 2003 +0200
+++ b/src/HOL/Algebra/Module.thy	Mon May 05 10:53:27 2003 +0200
@@ -139,7 +139,9 @@
   finally show ?thesis .
 qed
 
-subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
+subsection {* Every Abelian Group is a Z-module *}
+
+(* Not all versions of pdflatex permit $\mathbb{Z}$ in bookmarks. *)
 
 text {* Not finished. *}