src/HOL/Isar_examples/document/style.tex
changeset 7874 180364256231
parent 7869 c007f801cd59
child 7968 964b65b4e433
equal deleted inserted replaced
7873:5d1200c7a671 7874:180364256231
     7 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     7 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     8 
     8 
     9 \newcommand{\name}[1]{\textsl{#1}}
     9 \newcommand{\name}[1]{\textsl{#1}}
    10 
    10 
    11 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    11 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    12 \newcommand{\var}[1]{{?\!#1}}
    12 \newcommand{\var}[1]{{?\!\idt{#1}}}
    13 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    13 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    14 \newcommand{\dsh}{\dshsym}
    14 \newcommand{\dsh}{\dshsym}
    15 
    15 
    16 \newcommand{\To}{\to}
    16 \newcommand{\To}{\to}
    17 \newcommand{\dt}{{\mathpunct.}}
    17 \newcommand{\dt}{{\mathpunct.}}