# HG changeset patch
# User wenzelm
# Date 1209994033 -7200
# Node ID eee21d6d0a6be25c2504a8f9b9a58e8ba00a9147
# Parent  1651ff6a34b54c2d2403d4d5656a863170838470
removed isasymIN -- already defined in isar.sty;

diff -r 1651ff6a34b5 -r eee21d6d0a6b doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Mon May 05 15:23:59 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon May 05 15:27:13 2008 +0200
@@ -37,7 +37,6 @@
 \newcommand{\isasymASSUME}{\cmd{assume}}
 \newcommand{\isasymSHOW}{\cmd{show}}
 \newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymIN}{\cmd{in}}
 
 \newcommand{\qt}[1]{``#1''}
 \newcommand{\qtt}[1]{"{}{#1}"{}}
diff -r 1651ff6a34b5 -r eee21d6d0a6b doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon May 05 15:23:59 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon May 05 15:27:13 2008 +0200
@@ -31,7 +31,6 @@
 \newcommand{\isasymASSUME}{\cmd{assume}}
 \newcommand{\isasymSHOW}{\cmd{show}}
 \newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymIN}{\cmd{in}}
 \newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
 \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
 \newcommand{\isasymCODECONST}{\cmd{code\_const}}
diff -r 1651ff6a34b5 -r eee21d6d0a6b doc-src/IsarAdvanced/Functions/functions.tex
--- a/doc-src/IsarAdvanced/Functions/functions.tex	Mon May 05 15:23:59 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/functions.tex	Mon May 05 15:27:13 2008 +0200
@@ -33,7 +33,6 @@
 \newcommand{\isasymASSUME}{\cmd{assume}}
 \newcommand{\isasymSHOW}{\cmd{show}}
 \newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymIN}{\cmd{in}}
 \newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
 \newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
 \newcommand{\isasymFUN}{\cmd{fun}}