From f5708603f309bf12ac31c15ebedfdaf8e879283e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Nov 2005 12:59:41 +0000 Subject: [PATCH] some more on tinycals --- helm/papers/matita/matita.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index b356ddc55..b17ead736 100644 --- 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 -- 2.39.2