update in ground_2

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

diff --git a/matita/matita/nlibrary/re/re.ma b/matita/matita/nlibrary/re/re.ma
index 40947401f860939ceea720b2363c394a9671aef7..d0690ca26f2bd6d4d6bfa9431fd0709161d1794b 100644 (file)
--- a/matita/matita/nlibrary/re/re.ma
+++ b/matita/matita/nlibrary/re/re.ma
@@ -41,7 +41,7 @@ notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
 interpretation "or" 'plus a b = (o ? a b).
            
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}.
 interpretation "cat" 'pc a b = (c ? a b).
 
 (* to get rid of \middot *)
@@ -193,7 +193,7 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
 nqed.
 
 ndefinition lo ≝ λS:Alpha.λ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).
 
 ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
@@ -202,9 +202,9 @@ ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
    [ false ⇒ 〈e1 · \fst b, \snd b〉 
    | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
    
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}.
 interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
+notation > "a ⊙ b" left associative with precedence 65 for @{'lc eclose $a $b}.
 
 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
    match a with [ mk_pair e1 b1 ⇒
@@ -216,7 +216,7 @@ notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
 interpretation "lk" 'lk op a = (lk ? op a).
 notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
 
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation > "•" non associative with precedence 65 for @{eclose ?}.
 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
  match E with
   [ pz ⇒ 〈 ∅, false 〉
@@ -226,9 +226,9 @@ nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
   | po E1 E2 ⇒ •E1 ⊕ •E2
   | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 
   | pk E ⇒ 〈(\fst (•E))^*,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).
-notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+notation > "• x" non associative with precedence 65 for @{'eclose $x}.
 
 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 interpretation "reclose" 'eclose x = (reclose ? x).
@@ -525,7 +525,7 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |
 STOP
 
 notation > "\move term 90 x term 90 E" 
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
 nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
  match E with
   [ pz ⇒ 〈 ∅, false 〉
@@ -535,8 +535,8 @@ nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
   | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 
   | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
   | pk e ⇒ (\move x e)^⊛ ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
 interpretation "move" 'move x E = (move ? x E).
 
 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
@@ -606,7 +606,7 @@ ntheorem move_ok:
 nqed.
 
 
-notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}.
 nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
  match w with
   [ nil ⇒ E