X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=078c7fb00fe0489c74a9028d878198cdb386225d;hb=54e651eaa3cbcc16cfdf3fcc8b53482bffc78b76;hp=3a5bca154955900e112ae9f7828e0f078c3cd129;hpb=9449ec60150ea2326d7b54ad9c4f51e36d06bb65;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 3a5bca154..078c7fb00 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -124,14 +124,16 @@ far seguire le parentesi quadre come spiegato in precedenza.
 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
 
-Per motivi che saranno più chiari una volta studiate logiche del primo ordine
-o di ordine superiore, i lemmi che si intende riutilizzare è bene
-che siano dimostrati astratti sugli atomi, ovvero per ogni
-atomo `A`...`Z` che compare nella formula, è bene aggiungere
-una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`)
-e iniziare la dimostrazione con il comando `assume`. In tale
-modo il lemma EM può essere utilizzato sia per dimostrare 
-`A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ...
+Per motivi che saranno più chiari una volta studiate logiche del 
+primo ordine o di ordine superiore, i lemmi che si intende 
+riutilizzare è bene che siano dimostrati astratti sugli atomi. 
+Ovvero per ogni atomo `A`...`Z` che compare nella formula, 
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`. 
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare 
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
 
 DOCEND*)