From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 15:27:22 +0000 (+0000)
Subject: fixed or-in-left
X-Git-Tag: make_still_working~4552
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5978b976f9e1a2679e2b4ecc3c9984afdf2d5e11;p=helm.git

fixed or-in-left
---

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index b7ee07cb6..8a7399167 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -285,7 +285,7 @@ interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
   (show ab (Or_intro_l _ _ a)).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
-for @{ 'Or_intro_l_ok_1 $a $ab }.
+for @{ 'Or_intro_l_ok_2 $a $ab }.
 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
   (cast _ _ (show ab (Or_intro_l _ _ a))).