\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate
authorwenzelm
Sat, 05 Jan 2002 01:18:54 +0100
changeset 12638 812ce0d9fc85
parent 12637 4d43b06a81e1
child 12639 71605f976d50
\newcommand{\isasymignore}{}, so we may use \<ignore> to disambiguate duplicate syntax declarations for demonstration purposes;
doc-src/TutorialI/tutorial.sty
--- a/doc-src/TutorialI/tutorial.sty	Sat Jan 05 01:17:48 2002 +0100
+++ b/doc-src/TutorialI/tutorial.sty	Sat Jan 05 01:18:54 2002 +0100
@@ -68,6 +68,7 @@
 \newcommand{\ttEXU}{\texttt{EX!}}
 \newcommand{\ttAnd}{\texttt{!!}}
 
+\newcommand{\isasymignore}{}
 \newcommand{\isasymimp}{\isasymlongrightarrow}
 \newcommand{\isasymImp}{\isasymLongrightarrow}
 \newcommand{\isasymFun}{\isasymRightarrow}