From: Enrico Tassi Date: Fri, 18 Nov 2005 12:59:41 +0000 (+0000) Subject: some more on tinycals X-Git-Tag: V_0_7_2_3~40 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f5708603f309bf12ac31c15ebedfdaf8e879283e some more on tinycals --- 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