src/HOL/Real/HahnBanach/document/notation.tex
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
child 9278 0b8e87bb91d9
     1.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Sat Oct 30 20:21:46 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Sat Oct 30 20:32:04 1999 +0200
     1.3 @@ -1,10 +1,8 @@
     1.4  
     1.5  \renewcommand{\isamarkupheader}[1]{\section{#1}}
     1.6 -\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
     1.7  \newcommand{\isasymprod}{\emph{$\mult$}}
     1.8  \newcommand{\isasymzero}{\emph{$\zero$}}
     1.9  
    1.10 -
    1.11  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    1.12  \newcommand{\var}[1]{{?\!#1}}
    1.13  \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}