nasty change in the lexer/parser:

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

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 82e3b83fddabff7145544acec8333a8c77c42bf9..9768e26e2997da01f7c6b1da99a4cdff2ae1c174 100644 (file)
--- 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]);
              ]