nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
index 2c796236ddfc022e9829170cbbf1ae27927be00e..306818ab54f0b77e684201f4e1202229dd0a2756 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.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:
 
-        aply rule (∨_e (A∨B) [h1] C [h2] C);
+        aply 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)
@@ -165,20 +165,20 @@ theorem EM: ∀A:CProp. A ∨ ¬ A.
 assume A: CProp.
 apply rule (prove (A ∨ ¬A));
 apply rule (RAA [H] (⊥)).
-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
         [ apply rule (discharge [H]).
-        | apply rule (⊥_e (⊥));
-          apply rule (¬_e (¬¬A) (¬A));
-           [ apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+        | apply rule (⊥#e (⊥));
+          apply rule (¬#e (¬¬A) (¬A));
+           [ apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
               [ apply rule (discharge [H]).
-              | apply rule (∨_i_r (¬A)).
+              | apply rule (∨#i_r (¬A)).
           apply rule (discharge [K]).
               ]
-           | apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+           | apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
               [ apply rule (discharge [H]).
-              | apply rule (∨_i_l (A)).
+              | apply rule (∨#i_l (A)).
           apply rule (discharge [K]).
               ]
            ]
@@ -189,12 +189,12 @@ qed.
 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
 (*BEGIN*)
-apply rule (⇒_i [h1] (∀x.¬ P x));
-apply rule (∀_i {l} (¬P l));
-apply rule (¬_i [h2] (⊥));
-apply rule (¬_e (¬(∃x.P x)) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.¬ P x));
+apply rule (∀#i {l} (¬P l));
+apply rule (¬#i [h2] (⊥));
+apply rule (¬#e (¬(∃x.P x)) (∃x.P x));
        [ apply rule (discharge [h1]);
-       | apply rule (∃_i {l} (P l));
+       | apply rule (∃#i {l} (P l));
          apply rule (discharge [h2]);
        ]
 (*END*)
@@ -204,15 +204,15 @@ qed.
 lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
 apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
 (*BEGIN*)
-apply rule (⇒_i [h1] (∃x.¬ P x));
+apply rule (⇒#i [h1] (∃x.¬ P x));
 apply rule (RAA [h2] (⊥));
-apply rule (¬_e (¬(∀x.P x)) (∀x.P x));
+apply rule (¬#e (¬(∀x.P x)) (∀x.P x));
        [ apply rule (discharge [h2]);
-       | apply rule (∀_i {y} (P y));
+       | apply rule (∀#i {y} (P y));
     apply rule (RAA [h3] (⊥));
-    apply rule (¬_e (¬∃x.¬ P x) (∃x.¬ P x));
+    apply rule (¬#e (¬∃x.¬ P x) (∃x.¬ P x));
           [ apply rule (discharge [h2]);
-          | apply rule (∃_i {y} (¬P y));
+          | apply rule (∃#i {y} (¬P y));
        apply rule (discharge [h3]);
           ]
        ]
@@ -223,12 +223,12 @@ qed.
 lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
 apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
 (*BEGIN*)
-apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
-apply rule (∀_i {l} (P l ⇒ Q c));
-apply rule (⇒_i [h2] (Q c));
-apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.P x ⇒ Q c));
+apply rule (∀#i {l} (P l ⇒ Q c));
+apply rule (⇒#i [h2] (Q c));
+apply rule (⇒#e ((∃x.P x) ⇒ Q c) (∃x.P x));
        [ apply rule (discharge [h1]);
-       | apply rule (∃_i {l} (P l));
+       | apply rule (∃#i {l} (P l));
          apply rule (discharge [h2]);
        ]
 (*END*)
@@ -238,22 +238,22 @@ qed.
 lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
 apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
 (*BEGIN*)
-apply rule (⇒_i [h1] (∃x.P x ⇒ Q c));
-apply rule (∨_e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
+apply rule (⇒#i [h1] (∃x.P x ⇒ Q c));
+apply rule (∨#e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
        [ apply rule (lem 0 EM);
-       | apply rule (∃_i {y} (P y ⇒ Q c));
-       apply rule (⇒_i [h4] (Q c));
-       apply rule (⇒_e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
+       | apply rule (∃#i {y} (P y ⇒ Q c));
+       apply rule (⇒#i [h4] (Q c));
+       apply rule (⇒#e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
               [ apply rule (discharge [h1]);
          | apply rule (discharge [h3]);
               ]
-  | apply rule (∃_e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
+  | apply rule (∃#e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
           [ apply rule (lem 1 ex2 (¬(∀x.P x)));
             apply rule (discharge [h3]);
-     | apply rule (∃_i {y} (P y ⇒ Q c));
-       apply rule (⇒_i [h5] (Q c));
-       apply rule (⊥_e (⊥));
-       apply rule (¬_e (¬P y) (P y));
+     | apply rule (∃#i {y} (P y ⇒ Q c));
+       apply rule (⇒#i [h5] (Q c));
+       apply rule (⊥#e (⊥));
+       apply rule (¬#e (¬P y) (P y));
               [ apply rule (discharge [h4]);
               | apply rule (discharge [h5]);
               ]