exercises ready

[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 98142db2fd7f19ea8462c81839918798f538f8c2..5e71888149f9047fcab44fe45da3a8a8798e9c56 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -29,6 +29,18 @@ Per digitare i connettivi logici:
 * `⊥` : `\bot`
 * `⊤` : `\top`
 
+I termini, le formule e i nomi delle ipotesi
+============================================
+
+* I termini quantificati da `∀` e `∃`, quando argomenti di
+  una regola, vengono scritti tra `{` e `}`.
+
+* Le formule, quando argomenti di
+  una regola, vengono scritti tra `(` e `)`.
+
+* I nomi delle ipotesi, quando argomenti di
+  una regola, vengono scritti tra `[` e `]`.
+
 Le regole di deduzione naturale
 ===============================
 
@@ -75,7 +87,7 @@ DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
 
-theorem EM: ∀A. A ∨ ¬ A.
+theorem EM: ∀A:CProp. A ∨ ¬ A.
 (* Il comando assume è necessario perchè dimostriamo A∨¬A
    per una A generica. *)
 assume A: CProp.