From 0b9d417be5c46dacd7107f2e50539b6114ce9341 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Jul 2008 15:11:22 +0000
Subject: [PATCH] ...

---
 .../matita/library/demo/natural_deduction.ma  | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index 68d7327fd..4f9d70ffc 100644
--- 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 ≝
-- 
2.39.2