]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/dama/dama/uniform.ma
gran casino
[helm.git] / helm / software / matita / contribs / dama / dama / uniform.ma
index 25cfe67cb6da3e02adbfd4283078c1f619708d21..348b99a8139cf14e3a0f8cf05ea321d99a633342 100644 (file)
@@ -31,7 +31,7 @@ notation "a \subseteq u" left associative with precedence 70
   for @{ 'subset $a $u }.
 interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
-notation "hvbox({ ident x : t | break p })" non associative with precedence 50
+notation "hvbox({ ident x : t | break p })" non associative with precedence 80
   for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
 definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
 interpretation "explicit set" 'explicitset t = (mk_set _ t).