...

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 99a0e8a5a07b55768b5266f4a799f3de965e4419..bc52a8246f2521c3e1b5483ad2f87ef259e24a51 100644 (file)
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -30,7 +30,7 @@ Come scrivere i simboli
 =======================
 
 Per inserire i simboli matematici è necessario digitare il loro nome
-e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
+e poi premere ALT-L. In generale i nomi dei simboli sono della forma
 `\nome`, ad esempio `\equiv`. Alcuni simboli molto frequenti hanno
 dei sinonimi più comodi da digitare, per esemio `⇒` ha sia il nome
 `\Rightarrow` sia `=>`.
@@ -46,7 +46,7 @@ l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`.
 * `≡` : `\equiv`
 * `∀` : `\forall`
 
-La sintassi `∀v.P` significa "per tutti i `v` vale `P`".
+La sintassi `∀x.P` significa "per tutti gli `x` vale `P`".
 
 La sintassi `F → G` dove `F` e `G` sono proposizioni nel metalinguaggio
 significa "`F` implica `G`". Attenzione, il simbolo `⇒` (usato a lezione)
@@ -346,8 +346,9 @@ Tale linguaggio è composto dai seguenti comandi:
 
   Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi
   della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio
-  se la tesi fosse `sin π + 3 = 3` e si avesse una ipotesi `sin π = 0` dal
-  nome `H`, si potrebbe usare il comando `conclude (0 + 3) = 3 by H`.
+  se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
+  nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
+  per cambiare la conclusione in `0 + 3 = 7 - 4`.
 
 * `= (P) by name`