# HG changeset patch
# User wenzelm
# Date 979154410 -3600
# Node ID f2ffa2d97533d4c100880e6936a6d1124bac751f
# Parent  12f45010ecb544e6cb56d3992b79a708f5bb3b00
updated;

diff -r 12f45010ecb5 -r f2ffa2d97533 doc-src/AxClass/generated/isabelle.sty
--- 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)
 %%
diff -r 12f45010ecb5 -r f2ffa2d97533 doc-src/AxClass/generated/isabellesym.sty
--- 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}}
+
diff -r 12f45010ecb5 -r f2ffa2d97533 doc-src/TutorialI/isabellesym.sty
--- 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}}
+