src/HOL/Isar_examples/document/style.tex
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8020 2823ce1753a5
permissions -rw-r--r--
improved presentation;
wenzelm@7761
     1
wenzelm@7761
     2
%% $Id$
wenzelm@7748
     3
wenzelm@7748
     4
\documentclass[11pt,a4paper]{article}
wenzelm@7982
     5
\usepackage{comment,proof,isabelle,isabellesym,pdfsetup}
wenzelm@7748
     6
wenzelm@7748
     7
\renewcommand{\isamarkupheader}[1]{\section{#1}}
wenzelm@7748
     8
wenzelm@7833
     9
\newcommand{\name}[1]{\textsl{#1}}
wenzelm@7748
    10
wenzelm@7748
    11
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
wenzelm@7874
    12
\newcommand{\var}[1]{{?\!\idt{#1}}}
wenzelm@7748
    13
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
wenzelm@7748
    14
\newcommand{\dsh}{\dshsym}
wenzelm@7748
    15
wenzelm@7748
    16
\newcommand{\To}{\to}
wenzelm@7748
    17
\newcommand{\dt}{{\mathpunct.}}
wenzelm@7748
    18
\newcommand{\ap}{\mathbin{\!}}
wenzelm@7748
    19
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
wenzelm@7748
    20
\newcommand{\all}[1]{\forall #1\dt\;}
wenzelm@7748
    21
\newcommand{\ex}[1]{\exists #1\dt\;}
wenzelm@7817
    22
\newcommand{\impl}{\rightarrow}
wenzelm@7817
    23
\newcommand{\conj}{\land}
wenzelm@7833
    24
\newcommand{\disj}{\lor}
wenzelm@7968
    25
\newcommand{\Impl}{\Longrightarrow}
wenzelm@7817
    26
wenzelm@7748
    27
%%% Local Variables: 
wenzelm@7748
    28
%%% mode: latex
wenzelm@7748
    29
%%% TeX-master: "root"
wenzelm@7748
    30
%%% End: