...

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index 68d7327fdfab44f028e20747980b140f71cb0ff7..4f9d70ffc69d348161fe84ea01d75bd960562c04 100644 (file)
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -28,7 +28,7 @@ inductive Imply (A,B:CProp) : CProp ≝
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "Imply" 'Imply a b = (Imply a b).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i) " with precedence 19 for @{ 'Imply_intro $ab (λ${ident H}:$p.$b) }.
+notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19 for @{ 'Imply_intro $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro" 'Imply_intro ab \eta.b = (cast ab (Imply_intro _ _ b)).
 
 definition Imply_elim ≝ λA,B.λf:Imply A B.λa:A.match f with [ Imply_intro g ⇒ g a].
@@ -72,31 +72,36 @@ definition Or_elim ≝
  λA,B,C:CProp.λc:A∨B.λfa: A → C.λfb: B → C.
   match c with [ Or_intro_l a ⇒ fa a | Or_intro_r b ⇒ fb b].
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e)" with precedence 19 for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
-interpretation "Or_elim" 'Or_elim ab ac bc c = (cast c (Or_elim _ _ _ ab ac bc)).
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim" 'Or_elim ab \eta.ac \eta.bc c = (cast c (Or_elim _ _ _ ab ac bc)).
 
 inductive Exists (A:Type) (P:A→CProp) : CProp ≝
   Exists_intro: ∀w:A. P w → Exists A P.
 
 interpretation "constructive ex" 'exists \eta.x = (Exists _ x).
 
-notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19 for @{ 'Exists_intro $Pn $Px }.
+notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
+for @{ 'Exists_intro $Pn $Px }.
 interpretation "Exists_intro" 'Exists_intro Pn Px = (cast Px (Exists_intro _ _ _ Pn)).
 
 definition Exists_elim ≝
   λA:Type.λP:A→CProp.λC:CProp.λc:∃x:A.P x.λH:(∀x.P x → C).
    match c with [ Exists_intro w p ⇒ H w p ].
 
-notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e)" with precedence 19 for @{ 'Exists_elim $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
+notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
+for @{ 'Exists_elim $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim" 'Exists_elim ExPx Pc c = (cast c (Exists_elim _ _ _ ExPx Pc)).
 
 inductive Forall (A:Type) (P:A→CProp) : CProp ≝
  Forall_intro: (∀n:A. P n) → Forall A P.
 
-notation "\forall ident x:A.break term 19 Px" with precedence 20 for @{ 'Forall (λ${ident x}:$A.$Px) }.
+notation "\forall ident x:A.break term 19 Px" with precedence 20
+for @{ 'Forall (λ${ident x}:$A.$Px) }.
 interpretation "Forall" 'Forall \eta.Px = (Forall _ Px).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i)" with precedence 19 for @{ 'Forall_intro (λ${ident x}:$tx.$Px) $Pn }.
+notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
+for @{ 'Forall_intro (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro" 'Forall_intro Px Pn = (cast Pn (Forall_intro _ _ Px)).
 
 definition Forall_elim ≝