]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed notation
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 14 Nov 2007 13:21:06 +0000 (13:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 14 Nov 2007 13:21:06 +0000 (13:21 +0000)
helm/software/matita/dama/excedence.ma

index 59b8baa4ed1668cae080c58dcaec9cb1fcc99f39..4931e70d2ab2476131c78fac4d845dcbc4951df4 100644 (file)
@@ -51,7 +51,7 @@ record apartness : Type ≝ {
   ap_cotransitive: cotransitive ? ap_apart
 }.
 
-notation "a # b" non associative with precedence 50 for @{ 'apart $a $b}.
+notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}.
 interpretation "axiomatic apartness" 'apart x y = 
   (cic:/matita/excedence/ap_apart.con _ x y).
 
@@ -71,7 +71,7 @@ coercion cic:/matita/excedence/apart_of_excedence.con.
 
 definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
 
-notation "a ≈ b" non associative with precedence 50 for @{ 'napart $a $b}.    
+notation "a break ≈ b" non associative with precedence 50 for @{ 'napart $a $b}.    
 interpretation "alikeness" 'napart a b =
   (cic:/matita/excedence/eq.con _ a b).