src/HOL/Isar_examples/document/style.tex
author wenzelm
Sun, 26 Mar 2000 20:16:34 +0200
changeset 8584 016314c2fa0a
parent 8020 2823ce1753a5
child 9659 b9cf6801f3da
permissions -rw-r--r--
tuned;


%% $Id$

\documentclass[11pt,a4paper]{article}
\usepackage{proof,isabelle,isabellesym,pdfsetup}

\renewcommand{\isamarkupheader}[1]{\section{#1}}

\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}{\rightarrow}
\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: