X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcontribs%2FRELATIONAL%2FBNot%2Fdefs.ma;h=401e599a758605954b9ce8f5855b2c87bf66d8c2;hb=e21d67b7a00f768b085ecaa11d9a080f8ceb70d9;hp=d622645134a57163096cebb2fc70999a38231aaf;hpb=c86f1a6c4d00f66a81c576589f215cb667595710;p=helm.git

diff --git a/matita/contribs/RELATIONAL/BNot/defs.ma b/matita/contribs/RELATIONAL/BNot/defs.ma
index d62264513..401e599a7 100644
--- a/matita/contribs/RELATIONAL/BNot/defs.ma
+++ b/matita/contribs/RELATIONAL/BNot/defs.ma
@@ -14,9 +14,20 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/BNot/defs".
 
+include "logic/equality.ma".
+
 include "Bool/defs.ma".
 
 inductive BNot: Bool \to Bool \to Prop \def
    | bnot_false: BNot false true
    | bnot_true : BNot true false
 .
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "boolean not predicate" 'rel_not x y = 
+   (cic:/matita/RELATIONAL/BNot/defs/BNot.ind#xpointer(1/1) x y).
+
+(* FG: we can not use - here for some reason *)
+notation "hvbox(~ a break == b)" 
+  non associative with precedence 95
+for @{ 'rel_not $a $b}.