# HG changeset patch
# User wenzelm
# Date 1234814655 -3600
# Node ID ce2b8e6502f94457ecf9264aca6a811b1782d632
# Parent  df70c029157950ce82a370f1f360ef4ca584d701
removed unused glossary macros;

diff -r df70c0291579 -r ce2b8e6502f9 doc-src/IsarAdvanced/Functions/style.sty
--- a/doc-src/IsarAdvanced/Functions/style.sty	Mon Feb 16 20:49:39 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/style.sty	Mon Feb 16 21:04:15 2009 +0100
@@ -1,6 +1,3 @@
-
-%% $Id$
-
 %% toc
 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
@@ -10,13 +7,6 @@
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
-
 %% index
 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}