some more on tinycals

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index b356ddc5522edaf035147e91e6de0fb12294d6b9..b17ead7366de31c999a311be9d870ebb1a844ed5 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -1008,8 +1008,7 @@ The low-level tacticals implementation of \MATITA{} allows a step-by-step execut
   open the branching tactical \verb+[+. Then you can interact with the system
   reaching a proof of the first case, without having to specify the whole
   branching tactical. When you have proved all the induction cases, you close
-  the branching tactical with \verb+]+ and you are done with a structured proof
-  without the.
+  the branching tactical with \verb+]+ and you are done with a structured proof.
 \item[Rereading]
   is possible. Going on step by step shows exactly what is going on.
   Consider again a proof by induction, that starts applying the induction