# HG changeset patch
# User wenzelm
# Date 1455464383 -3600
# Node ID aaeee16a56f5edbdd034a2fcc58e48ed326d6d2a
# Parent  5e5a881ebc128edda046aa25626e2dd8666a90da
unused;

diff -r 5e5a881ebc12 -r aaeee16a56f5 src/HOL/Imperative_HOL/document/root.tex
--- 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}