update in ground_2

[helm.git] / matita / matita / re_complete / re.ma

diff --git a/matita/matita/re_complete/re.ma b/matita/matita/re_complete/re.ma
index ff1f959934f732abac43f6b7f4337099498e912d..5aff713ad292401de8cbda282f7cdae0b79892c5 100644 (file)
--- a/matita/matita/re_complete/re.ma
+++ b/matita/matita/re_complete/re.ma
@@ -231,7 +231,7 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
 qed.
 
 definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}.
 interpretation "oplus" 'oplus a b = (lo ? a b).
 
 lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
@@ -240,7 +240,7 @@ lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2
 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
   match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
  
-notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
+notation "i ◃ e" left associative with precedence 65 for @{'lhd $i $e}.
 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
 
 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. 
@@ -261,10 +261,10 @@ definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe
     ]
   ].
 
-notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+notation "a ▹ b" left associative with precedence 65 for @{'tril eclose $a $b}.
 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
 
-notation "•" non associative with precedence 60 for @{eclose ?}.
+notation "•" non associative with precedence 65 for @{eclose ?}.
 
 let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
  match i with
@@ -276,7 +276,7 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
   | pc i1 i2 ⇒ •i1 ▹ i2
   | pk i ⇒ 〈(\fst (•i))^*,true〉].
   
-notation "• x" non associative with precedence 60 for @{'eclose $x}.
+notation "• x" non associative with precedence 65 for @{'eclose $x}.
 interpretation "eclose" 'eclose x = (eclose ? x).
 
 lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.