
diff -r 6c13f76c070b -r 9580bae0500d thys3/document/root.tex
--- a/thys3/document/root.tex	Thu Feb 16 23:23:22 2023 +0000
+++ b/thys3/document/root.tex	Mon Feb 20 23:40:30 2023 +0000
@@ -53,6 +53,7 @@
 \newcommand{\ZERO}{\mbox{\bf 0}}
 \newcommand{\ONE}{\mbox{\bf 1}}
 \def\rs{\mathit{rs}}
+\definecolor{darkblue}{rgb}{0,0,0.6}
 
 \def\Brz{Brzozowski}
 \def\der{\backslash}




