--- a/src/HOL/Isar_examples/document/style.tex Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/document/style.tex Wed Nov 16 19:34:19 2005 +0100
@@ -3,6 +3,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage{ifthen,proof,isabelle,isabellesym}
+\isabellestyle{it}
\usepackage{pdfsetup}\urlstyle{rm}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
@@ -27,7 +28,7 @@
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
\newcommand{\all}[1]{\forall #1\dt\;}
\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\rightarrow}
+\newcommand{\impl}{\to}
\newcommand{\conj}{\land}
\newcommand{\disj}{\lor}
\newcommand{\Impl}{\Longrightarrow}