equal
deleted
inserted
replaced
83 \def\retrieve{\textit{retrieve}} |
83 \def\retrieve{\textit{retrieve}} |
84 \def\blexer{\textit{blexer}} |
84 \def\blexer{\textit{blexer}} |
85 \def\flex{\textit{flex}} |
85 \def\flex{\textit{flex}} |
86 \def\inj{\mathit{inj}} |
86 \def\inj{\mathit{inj}} |
87 \def\Empty{\textit{Empty}} |
87 \def\Empty{\textit{Empty}} |
88 \def\Left{\mathit{Left}} |
88 \def\Left{\textit{Left}} |
89 \def\Right{\mathit{Right}} |
89 \def\Right{\textit{Right}} |
90 \def\Stars{\mathit{Stars}} |
90 \def\Stars{\mathit{Stars}} |
91 \def\Char{\mathit{Char}} |
91 \def\Char{\mathit{Char}} |
92 \def\Seq{\mathit{Seq}} |
92 \def\Seq{\mathit{Seq}} |
93 \def\Der{\textit{Der}} |
93 \def\Der{\textit{Der}} |
94 \def\Ders{\textit{Ders}} |
94 \def\Ders{\textit{Ders}} |