# HG changeset patch
# User nipkow
# Date 1118085679 -7200
# Node ID cb0f9e96d456a673dc94f946bc8b67ea6834e855
# Parent  8117e2037d3b668e22117408c4626feb1c6ac415
*** empty log message ***

diff -r 8117e2037d3b -r cb0f9e96d456 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon Jun 06 21:20:54 2005 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Jun 06 21:21:19 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
+%% 
 
 %%% Simple document preparation (based on theory token language and symbols)
 
diff -r 8117e2037d3b -r cb0f9e96d456 doc-src/TutorialI/isabellesym.sty
--- a/doc-src/TutorialI/isabellesym.sty	Mon Jun 06 21:20:54 2005 +0200
+++ b/doc-src/TutorialI/isabellesym.sty	Mon Jun 06 21:21:19 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% 
 
 % symbol definitions
 
@@ -219,6 +220,7 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
 \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
 \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}