diff -r 5a1196466a9c -r e3eb82ea2244 thys/Paper/document/root.tex
--- a/thys/Paper/document/root.tex	Tue Mar 15 01:10:38 2016 +0000
+++ b/thys/Paper/document/root.tex	Wed Mar 16 07:15:12 2016 +0000
@@ -26,7 +26,7 @@
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-\renewcommand{\isacharprime}{\mbox{$\mbox{}\!\!\mbox{$^\prime$}$}}
+%%\renewcommand{\isacharprime}{\makebox[0mm]{$\mbox{}\mbox{$\,^\prime$}$}}
 
 \definecolor{mygrey}{rgb}{.80,.80,.80}
 \def\Brz{Brzozowski}