--- a/src/HOL/Isar_Examples/document/style.tex Mon Nov 02 16:17:09 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
-\isabellestyle{it}
-\usepackage{pdfsetup}\urlstyle{rm}
-
-\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}}}}
-\newcommand{\var}[1]{{?\!\idt{#1}}}
-\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
-\newcommand{\dsh}{\dshsym}
-
-\newcommand{\To}{\to}
-\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\ap}{\mathbin{\!}}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\to}
-\newcommand{\conj}{\land}
-\newcommand{\disj}{\lor}
-\newcommand{\Impl}{\Longrightarrow}
-
-\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: