From d5b0c5c4409e789df8629943de2344a54b64686b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 18 Oct 2008 19:38:56 +0000 Subject: [PATCH] ... --- helm/software/matita/contribs/didactic/induction.ma | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index 99a0e8a5a..bc52a8246 100644 --- 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` -- 2.39.2