src/HOL/Isar_examples/document/style.tex
changeset 7833 f5288e4b95d1
parent 7817 76cffd7dff2e
child 7869 c007f801cd59
equal deleted inserted replaced
7832:77bac5d84162 7833:f5288e4b95d1
     1 
     1 
     2 %% $Id$
     2 %% $Id$
     3 
     3 
     4 \documentclass[11pt,a4paper]{article}
     4 \documentclass[11pt,a4paper]{article}
     5 \usepackage{comment,isabelle,pdfsetup}
     5 \usepackage{comment,proof,isabelle,pdfsetup}
     6 
     6 
     7 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     7 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     8 \parindent 0pt \parskip 0.5ex
     8 \parindent 0pt \parskip 0.5ex
     9 
     9 
    10 \newcommand{\name}[1]{\textsf{#1}}
    10 \newcommand{\name}[1]{\textsl{#1}}
    11 
    11 
    12 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    12 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    13 \newcommand{\var}[1]{{?\!#1}}
    13 \newcommand{\var}[1]{{?\!#1}}
    14 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    14 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    15 \newcommand{\dsh}{\dshsym}
    15 \newcommand{\dsh}{\dshsym}
    20 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
    20 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
    21 \newcommand{\all}[1]{\forall #1\dt\;}
    21 \newcommand{\all}[1]{\forall #1\dt\;}
    22 \newcommand{\ex}[1]{\exists #1\dt\;}
    22 \newcommand{\ex}[1]{\exists #1\dt\;}
    23 \newcommand{\impl}{\rightarrow}
    23 \newcommand{\impl}{\rightarrow}
    24 \newcommand{\conj}{\land}
    24 \newcommand{\conj}{\land}
       
    25 \newcommand{\disj}{\lor}
    25 
    26 
    26 
    27 
    27 %%% Local Variables: 
    28 %%% Local Variables: 
    28 %%% mode: latex
    29 %%% mode: latex
    29 %%% TeX-master: "root"
    30 %%% TeX-master: "root"