src/HOL/Isar_examples/document/style.tex
changeset 10146 e89309dde9d3
parent 9659 b9cf6801f3da
child 18193 54419506df9e
--- a/src/HOL/Isar_examples/document/style.tex	Tue Oct 03 22:35:44 2000 +0200
+++ b/src/HOL/Isar_examples/document/style.tex	Tue Oct 03 22:36:22 2000 +0200
@@ -2,11 +2,18 @@
 %% $Id$
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{proof,isabelle,isabellesym,pdfsetup}
-\urlstyle{rm}
+\usepackage{ifthen,proof,isabelle,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
 
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+
+\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
+
 \newcommand{\name}[1]{\textsl{#1}}
 
 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}