]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed some (more) typos
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Sep 2005 14:16:28 +0000 (14:16 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 30 Sep 2005 14:16:28 +0000 (14:16 +0000)
helm/ocaml/tactics/doc/main.tex

index b2996c11609edd25e076723cadd197b181ff3a1e..1cc0dadd99e6fa090ef4e4e082ed3f99975b1254 100644 (file)
  & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
  \\[1ex]
 
- \multicolumn{3}{l}{\hspace{2em}
+ \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
  \left\{
  \begin{array}{rcll}
   \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
   & =
   & \langle\xi_i, G^O_i, G^C_i\rangle
-  & g_i\in G^C_i \\
+  & g_{i+1}\in G^C_i \\
   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
   & =
   & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
-  & g_i\not\in G^C_i \\
+  & g_{i+1}\not\in G^C_i \\
   & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
   \\
  \end{array}