author wenzelm Sun, 21 Mar 2021 23:24:20 +0100 changeset 73463 552a9dd5b4a2 parent 73462 8995cab6b7a6 child 73464 b138cdd22cfb
prefer isabelle bbbfont;
 src/HOL/Matrix_LP/Matrix.thy file | annotate | diff | comparison | revisions src/HOL/Matrix_LP/document/root.tex file | annotate | diff | comparison | revisions src/HOL/ZF/document/root.tex file | annotate | diff | comparison | revisions
--- 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.$
--- 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}
--- 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}