nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
index f4508923730b134f904b4f89baa401b4c83fc506..4a65968db6159a0a96b62a7e879455ff47e27929 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
@@ -41,20 +41,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]).
              ]
           ]
@@ -64,29 +64,29 @@ qed.
 theorem ex0 : (F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E.
 apply rule (prove ((F∧¬G ⇒ L ⇒ E) ⇒ (G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
-apply rule (⇒_i [h2] (F ∧ L ⇒ E));
-apply rule (⇒_i [h3] (E));
-apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
+apply rule (⇒#i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
+apply rule (⇒#i [h2] (F ∧ L ⇒ E));
+apply rule (⇒#i [h3] (E));
+apply rule (∨#e (G∨¬G) [h4] (E) [h4] (E));
        [ apply rule (lem 0 EM);
-       | apply rule (⇒_e (G∧L⇒E) (G∧L));
+       | apply rule (⇒#e (G∧L⇒E) (G∧L));
            [ apply rule (discharge [h2]);
-           | apply rule (∧_i (G) (L));
+           | apply rule (∧#i (G) (L));
                [ apply rule (discharge [h4]);
-               | apply rule (∧_e_r (F∧L));
+               | apply rule (∧#e_r (F∧L));
                  apply rule (discharge [h3]);
                ]
            ]
-       | apply rule (⇒_e (L⇒E) (L));
-           [ apply rule (⇒_e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
+       | apply rule (⇒#e (L⇒E) (L));
+           [ apply rule (⇒#e (F∧¬G ⇒ L ⇒ E) (F∧¬G));
                [ apply rule (discharge [h1]);
-               | apply rule (∧_i (F) (¬G));
-                   [ apply rule (∧_e_l (F∧L));
+               | apply rule (∧#i (F) (¬G));
+                   [ apply rule (∧#e_l (F∧L));
                      apply rule (discharge [h3]);
                    | apply rule (discharge [h4]);
                    ]
                ]  
-           | apply rule (∧_e_r (F∧L));
+           | apply rule (∧#e_r (F∧L));
              apply rule (discharge [h3]);
            ]
        ]
@@ -96,29 +96,29 @@ qed.
 theorem ex1 : (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E.
 apply rule (prove (F ⇒ G∨E) ⇒ (G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E);
 (*BEGIN*)
-apply rule (⇒_i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (¬L∨F) [h5] (E) [h5] (E));
+apply rule (⇒#i [h1] ((G ⇒ ¬ (L ∧ ¬E)) ⇒ (¬L ∨ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((¬L ∨ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (¬L∨F) [h5] (E) [h5] (E));
        [ apply rule (discharge [h3]);
-       | apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬L) (L));
+       | apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬L) (L));
            [ apply rule (discharge [h5]);
            | apply rule (discharge [h4]);
            ]
-       | apply rule (∨_e (G∨E) [h6] (E) [h6] (E));
-          [ apply rule (⇒_e (F⇒G∨E) (F));
+       | apply rule (∨#e (G∨E) [h6] (E) [h6] (E));
+          [ apply rule (⇒#e (F⇒G∨E) (F));
              [ apply rule (discharge [h1]);
              | apply rule (discharge [h5]);
              ]
           | apply rule (RAA [h7] (⊥));
-       apply rule (¬_e (¬ (L ∧ ¬E)) (L ∧ ¬E));
-              [ apply rule (⇒_e (G ⇒ ¬ (L ∧ ¬E)) (G));
+       apply rule (¬#e (¬ (L ∧ ¬E)) (L ∧ ¬E));
+              [ apply rule (⇒#e (G ⇒ ¬ (L ∧ ¬E)) (G));
                   [apply rule (discharge [h2]);
                   |apply rule (discharge [h6]);
                   ]
-              | apply rule (∧_i (L) (¬E));
+              | apply rule (∧#i (L) (¬E));
                   [ apply rule (discharge [h4]);
                   | apply rule (discharge [h7]);
                   ]
@@ -132,29 +132,29 @@ qed.
 theorem ex2 : (F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E.
 apply rule (prove ((F∧G ⇒ E) ⇒ (H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
-apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
-apply rule (⇒_i [h3] (H ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
+apply rule (⇒#i [h1] ((H ⇒ E∨F) ⇒ (¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒#i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
+apply rule (⇒#i [h3] (H ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨¬G) [h5] (E) [h5] (E));
        [apply rule (lem 0 EM);
-       | apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
-          [ apply rule (⇒_e (H ⇒ E∨F) (H));
+       | apply rule (∨#e (E∨F) [h6] (E) [h6] (E));
+          [ apply rule (⇒#e (H ⇒ E∨F) (H));
               [ apply rule (discharge [h2]);
               | apply rule (discharge [h4]);
               ]
           | apply rule (discharge [h6]);
-          | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+          | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
              [apply rule (discharge [h1]);
-             |apply rule (∧_i (F) (G));
+             |apply rule (∧#i (F) (G));
                [ apply rule (discharge [h6]);
                | apply rule (discharge [h5]);
                ]
              ]
           ]
-       | apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬H) (H));
-       [ apply rule (⇒_e (¬G ⇒ ¬H) (¬G));
+       | apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬H) (H));
+       [ apply rule (⇒#e (¬G ⇒ ¬H) (¬G));
               [ apply rule (discharge [h3]);
               | apply rule (discharge [h5]);
               ]
@@ -167,22 +167,22 @@ qed.
 theorem ex3 : (F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E.
 apply rule (prove ((F∧G ⇒ E) ⇒ (¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E)).
 (*BEGIN*)
-apply rule (⇒_i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((L ⇒ F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
+apply rule (⇒#i [h1] ((¬E ⇒ G∨¬L) ⇒ (L ⇒ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L ⇒ F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
 apply rule (RAA [h5] (⊥));
-apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
-       [ apply rule (⇒_e (¬E ⇒ G∨¬L) (¬E));
+apply rule (∨#e (G∨¬L) [h6] (⊥) [h6] (⊥));
+       [ apply rule (⇒#e (¬E ⇒ G∨¬L) (¬E));
            [ apply rule (discharge [h2]);
            | apply rule (discharge [h5]);
            ]
-       | apply rule (¬_e (¬E) (E));
+       | apply rule (¬#e (¬E) (E));
        [ apply rule (discharge [h5]);
-           | apply rule (⇒_e (F∧G ⇒ E) (F∧G));
+           | apply rule (⇒#e (F∧G ⇒ E) (F∧G));
               [ apply rule (discharge [h1]);
-              | apply rule (∧_i (F) (G));
-                  [ apply rule (⇒_e (L⇒F) (L));
+              | apply rule (∧#i (F) (G));
+                  [ apply rule (⇒#e (L⇒F) (L));
                      [ apply rule (discharge [h3]);
                      | apply rule (discharge [h4]);
                      ]
@@ -190,7 +190,7 @@ apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥));
                   ]
               ]
            ]
-       | apply rule (¬_e (¬L) (L));
+       | apply rule (¬#e (¬L) (L));
            [ apply rule (discharge [h6]);
            | apply rule (discharge [h4]);
            ]