- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / nlibrary / logic / cprop.ma

diff --git a/matita/matita/nlibrary/logic/cprop.ma b/matita/matita/nlibrary/logic/cprop.ma
index e7ecf01ad5f47a49885a477b1b96138de00d893e..2c5303c5664d690ccc81d9583c01b81ffe44072a 100644 (file)
--- a/matita/matita/nlibrary/logic/cprop.ma
+++ b/matita/matita/nlibrary/logic/cprop.ma
@@ -39,7 +39,7 @@ ndefinition fi': ∀A,B:CPROP. A = B → B → A.
  #A; #B; #H; napply (fi … H); nassumption.
 nqed.
 
-notation ". r" with precedence 50 for @{'fi $r}.
+notation ". r" with precedence 55 for @{'fi $r}.
 interpretation "fi" 'fi r = (fi' ?? r).
 
 ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
@@ -227,7 +227,7 @@ nqed.
    - x1...xn are bound in E and P, H is bound in P
    - H is an identifier that will have the type of E in P
    - P is the proof that the two existentially quantified predicates are equal*)
-notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20 
+notation > "∑ list1 ident x sep , . term 61 E / ident nE ; term 19 H" with precedence 20 
 for @{ 'Sig_gen 
   ${ fold right @{ 'End }  rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
   ${ fold right @{ $E }              rec acc @{ λ${ident x}.$acc } } 
@@ -262,4 +262,4 @@ nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoi
    ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
 #S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
 *)
-  
\ No newline at end of file
+