--- a/doc-src/AxClass/generated/isabelle.sty Wed Jan 10 20:19:56 2001 +0100
+++ b/doc-src/AxClass/generated/isabelle.sty Wed Jan 10 20:20:10 2001 +0100
@@ -1,5 +1,4 @@
%%
-%% $Id$
%% Author: Markus Wenzel, TU Muenchen
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
--- a/doc-src/AxClass/generated/isabellesym.sty Wed Jan 10 20:19:56 2001 +0100
+++ b/doc-src/AxClass/generated/isabellesym.sty Wed Jan 10 20:20:10 2001 +0100
@@ -1,5 +1,4 @@
%%
-%% $Id$
%% Author: Markus Wenzel, TU Muenchen
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
@@ -289,4 +288,10 @@
\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
+\newcommand{\isasymwrong}{\isamath{\wr}}
\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+
--- a/doc-src/TutorialI/isabellesym.sty Wed Jan 10 20:19:56 2001 +0100
+++ b/doc-src/TutorialI/isabellesym.sty Wed Jan 10 20:20:10 2001 +0100
@@ -288,4 +288,10 @@
\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
+\newcommand{\isasymwrong}{\isamath{\wr}}
\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+