# HG changeset patch
# User wenzelm
# Date 1616365460 -3600
# Node ID 552a9dd5b4a249cafe04004ad7ef4f1f60b00360
# Parent  8995cab6b7a6aa3bcc0e61158f070135fac7f442
prefer isabelle bbbfont;

diff -r 8995cab6b7a6 -r 552a9dd5b4a2 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Sun Mar 21 23:16:34 2021 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Sun Mar 21 23:24:20 2021 +0100
@@ -282,8 +282,8 @@
 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
 
 text\<open>
-On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,
-as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have
+On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\bbbZ$, $B=\{-1, 0, 1\}$,
+as $f$ we take addition on $\bbbZ$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have
 \[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
 but on the other hand we have
 \[ f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.\]
diff -r 8995cab6b7a6 -r 552a9dd5b4a2 src/HOL/Matrix_LP/document/root.tex
--- a/src/HOL/Matrix_LP/document/root.tex	Sun Mar 21 23:16:34 2021 +0100
+++ b/src/HOL/Matrix_LP/document/root.tex	Sun Mar 21 23:24:20 2021 +0100
@@ -9,8 +9,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
-
 \begin{document}
 
 \title{Matrix}
diff -r 8995cab6b7a6 -r 552a9dd5b4a2 src/HOL/ZF/document/root.tex
--- a/src/HOL/ZF/document/root.tex	Sun Mar 21 23:16:34 2021 +0100
+++ b/src/HOL/ZF/document/root.tex	Sun Mar 21 23:24:20 2021 +0100
@@ -8,8 +8,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
-
 \begin{document}
 
 \title{ZF}