From 3585c1963c95d33f98367018119bfd4b3c6b99b2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 17:48:16 +0000 Subject: [PATCH 1/1] better spacing --- .../matita/library/didactic/support/natural_deduction.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index 9ae03f502..90ebd7217 100644 --- 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))). -- 2.39.2