X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction_theories.ma;h=9768e26e2997da01f7c6b1da99a4cdff2ae1c174;hb=b254cc57f5e082712f3ec6be9295eec0062b8d47;hp=82e3b83fddabff7145544acec8333a8c77c42bf9;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
index 82e3b83fd..9768e26e2 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma
@@ -71,7 +71,7 @@ L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
 Ad esempio: 
 
-        apply rule (∧_i (A∨B) ⊥);
+        apply rule (∧#i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 
@@ -81,7 +81,7 @@ gli argomenti delle regole sono le formule che normalmente
 scrivete sopra la linea che rappresenta l'applicazione della
 regola stessa. Ad esempio:
 
-        apply rule (∨_e (A∨B) [h1] C [h2] C);
+        apply rule (∨#e (A∨B) [h1] C [h2] C);
           [ …prova di (A∨B)
           | …prova di C sotto l'ipotesi A (di nome h1)  
           | …prova di C sotto l'ipotesi B (di nome h2)
@@ -238,27 +238,27 @@ apply rule (prove (∀x.x + O = x));
    l'unica forma di `apply rule lem` che potete usare è 
    `apply rule (lem 0 nome_assioma)` *)
 (*BEGIN*)
-apply rule (⇒_e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
-	[ apply rule (⇒_e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
+apply rule (⇒#e ((∀n.(n + O) = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (∀n.(n + O) = n ⇒ ((S n) + O) = (S n)));
+	[ apply rule (⇒#e ((O + O) = O ⇒ (∀n.n + O = n ⇒ ((S n) + O) = (S n)) ⇒ (∀x.(x + O) = x)) (O + O = O));
 	   [ apply rule (lem 0 induct);
-	   | apply rule (∀_e {O} (∀y.(O + y) =y));
+	   | apply rule (∀#e {O} (∀y.(O + y) =y));
 	     apply rule (lem 0 plus_O);
 	   ]
-	| apply rule (∀_i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
-    apply rule (⇒_i [H] (((S n) + O) = (S n)));
-    apply rule (⇒_e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
-	   [ apply rule (⇒_e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
-	      [ apply rule (∀_e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
-	        apply rule (∀_e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
-          apply rule (∀_e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
+	| apply rule (∀#i {n} (n + O = n ⇒ ((S n) + O) = (S n)));
+    apply rule (⇒#i [H] (((S n) + O) = (S n)));
+    apply rule (⇒#e ((S (n + O)) = (S n) ⇒ ((S n) + O) = (S n)) ((S (n + O)) = (S n)));
+	   [ apply rule (⇒#e (((S n) + O) =(S (n + O)) ⇒ (S (n + O)) = (S n)⇒((S n) + O) =(S n)) (((S n) + O) =(S (n + O))));
+	      [ apply rule (∀#e {S n} (∀z.((S n) + O) =(S (n + O))⇒(S (n + O))= z⇒((S n) + O) =z));
+	        apply rule (∀#e {(S (n + O))} (∀y.∀z.((S n) + O) =y ⇒ y = z ⇒ ((S n) + O) =z));
+          apply rule (∀#e {(S n) + O} (∀x.∀y.∀z.x = y ⇒ y = z ⇒ x = z));
           apply rule (lem 0 trans);
-	      | apply rule (∀_e {O} (∀m.(S n) + m = (S (n + m))));
-          apply rule (∀_e {n} (∀n.∀m.(S n) + m = (S (n + m))));
+	      | apply rule (∀#e {O} (∀m.(S n) + m = (S (n + m))));
+          apply rule (∀#e {n} (∀n.∀m.(S n) + m = (S (n + m))));
           apply rule (lem 0 plus_S);
 	      ]
-	   | apply rule (⇒_e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
-	      [ apply rule (∀_e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
-          apply rule (∀_e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
+	   | apply rule (⇒#e (n + O = n ⇒ (S (n + O)) = (S n)) (n + O = n));
+	      [ apply rule (∀#e {n} (∀w.n + O = w ⇒ (S (n + O)) = (S w)));
+          apply rule (∀#e {(n + O)} (∀y.∀w.y = w ⇒ (S y) = (S w)));
           apply rule (lem 0 eq_S);
 	      | apply rule (discharge [H]);
 	      ]