--- a/src/HOL/Imperative_HOL/document/root.tex Sun Feb 14 16:30:27 2016 +0100
+++ b/src/HOL/Imperative_HOL/document/root.tex Sun Feb 14 16:39:43 2016 +0100
@@ -1,4 +1,3 @@
-
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage{amssymb}
@@ -55,9 +54,6 @@
\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
-% Isar sorry
-\renewcommand{\isacommand}[1]{\ifthenelse{\equal{sorry}{#1}}{\isasymproof}{\isakeyword{#1}}}
-
\begin{document}