removed isasymIN -- already defined in isar.sty;
authorwenzelm
Mon, 05 May 2008 15:27:13 +0200
changeset 26784eee21d6d0a6b
parent 26783 1651ff6a34b5
child 26785 e77f9b8c7514
removed isasymIN -- already defined in isar.sty;
doc-src/IsarAdvanced/Classes/classes.tex
doc-src/IsarAdvanced/Codegen/codegen.tex
doc-src/IsarAdvanced/Functions/functions.tex
     1.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Mon May 05 15:23:59 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon May 05 15:27:13 2008 +0200
     1.3 @@ -37,7 +37,6 @@
     1.4  \newcommand{\isasymASSUME}{\cmd{assume}}
     1.5  \newcommand{\isasymSHOW}{\cmd{show}}
     1.6  \newcommand{\isasymNOTE}{\cmd{note}}
     1.7 -\newcommand{\isasymIN}{\cmd{in}}
     1.8  
     1.9  \newcommand{\qt}[1]{``#1''}
    1.10  \newcommand{\qtt}[1]{"{}{#1}"{}}
     2.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon May 05 15:23:59 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon May 05 15:27:13 2008 +0200
     2.3 @@ -31,7 +31,6 @@
     2.4  \newcommand{\isasymASSUME}{\cmd{assume}}
     2.5  \newcommand{\isasymSHOW}{\cmd{show}}
     2.6  \newcommand{\isasymNOTE}{\cmd{note}}
     2.7 -\newcommand{\isasymIN}{\cmd{in}}
     2.8  \newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
     2.9  \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
    2.10  \newcommand{\isasymCODECONST}{\cmd{code\_const}}
     3.1 --- a/doc-src/IsarAdvanced/Functions/functions.tex	Mon May 05 15:23:59 2008 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Functions/functions.tex	Mon May 05 15:27:13 2008 +0200
     3.3 @@ -33,7 +33,6 @@
     3.4  \newcommand{\isasymASSUME}{\cmd{assume}}
     3.5  \newcommand{\isasymSHOW}{\cmd{show}}
     3.6  \newcommand{\isasymNOTE}{\cmd{note}}
     3.7 -\newcommand{\isasymIN}{\cmd{in}}
     3.8  \newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
     3.9  \newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
    3.10  \newcommand{\isasymFUN}{\cmd{fun}}