better spacing

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 9ae03f502df8200fd670e8b8802a74c967545e10..90ebd7217751b6ab807fde4fc0b562307a6359ff 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -438,22 +438,22 @@ interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).
 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
 
 (* ¬ introduction *)
-notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
+notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = 
   (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
 
-notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = 
   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19
+notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = 
   (show ab (Not_intro _ b)).
 
-notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = 
   (cast _ _ (show ab (Not_intro _ b))).