X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fnatural_deduction.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fnatural_deduction.ma;h=9a7fd3671656547cb68fb7adfacc4e52c7cd2315;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=14359325b6509e4d7a59f61b7acf8d895a4fbcbf;hpb=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index 14359325b..9a7fd3671 100644
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -19,17 +19,17 @@ lemma RAA_to_EM : A ∨ ¬ A.
   apply rule (prove (A ∨ ¬ A));
   
   apply rule (RAA [H] ⊥);
-  apply rule (¬_e (¬A) A);
-    [ apply rule (¬_i [H1] ⊥);
-      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+  apply rule (¬#e (¬A) A);
+    [ apply rule (¬#i [H1] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
       [ apply rule (discharge [H]);
-      | apply rule (∨_i_l A);
+      | apply rule (∨#i_l A);
         apply rule (discharge [H1]);
       ]
     | apply rule (RAA [H2] ⊥);
-      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
       [ apply rule (discharge [H]);
-      | apply rule (∨_i_r (¬A));
+      | apply rule (∨#i_r (¬A));
         apply rule (discharge [H2]);
       ]
     ]
@@ -40,17 +40,17 @@ lemma RA_to_EM1 : A ∨ ¬ A.
   apply rule (prove (A ∨ ¬ A));
   
   apply rule (RAA [H] ⊥);
-  apply rule (¬_e (¬¬A) (¬A));
-    [ apply rule (¬_i [H2] ⊥);
-      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+  apply rule (¬#e (¬¬A) (¬A));
+    [ apply rule (¬#i [H2] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
       [ apply rule (discharge [H]);
-      | apply rule (∨_i_r (¬A));
+      | apply rule (∨#i_r (¬A));
         apply rule (discharge [H2]);
       ]
-    | apply rule (¬_i [H1] ⊥);
-      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+    | apply rule (¬#i [H1] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
       [ apply rule (discharge [H]);
-      | apply rule (∨_i_l A);
+      | apply rule (∨#i_l A);
         apply rule (discharge [H1]);
       ]
     ]
@@ -60,19 +60,19 @@ lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
 
  apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
    
- apply rule (⇒_i [H] (A∧C⇒E∧C∨B));
- apply rule (⇒_i [K] (E∧C∨B));
- apply rule (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
+ apply rule (⇒#i [H] (A∧C⇒E∧C∨B));
+ apply rule (⇒#i [K] (E∧C∨B));
+ apply rule (∨#e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
 [ apply rule (discharge [H]);
-| apply rule (∨_i_l (E∧C));
-  apply rule (∧_i E C);
-  [ apply rule (⇒_e (A⇒E) A);
+| apply rule (∨#i_l (E∧C));
+  apply rule (∧#i E C);
+  [ apply rule (⇒#e (A⇒E) A);
     [ apply rule (discharge [C1]);
-    | apply rule (∧_e_l (A∧C)); apply rule (discharge [K]);
+    | apply rule (∧#e_l (A∧C)); apply rule (discharge [K]);
     ]
-  | apply rule (∧_e_r (A∧C)); apply rule (discharge [K]);
+  | apply rule (∧#e_r (A∧C)); apply rule (discharge [K]);
   ]
-| apply rule (∨_i_r B); apply rule (discharge [C2]);
+| apply rule (∨#i_r B); apply rule (discharge [C2]);
 ]
 qed.