0.5.6 almost ok

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 3a5bca154955900e112ae9f7828e0f078c3cd129..078c7fb00fe0489c74a9028d878198cdb386225d 100644 (file)
--- 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*)