X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fbackground%2Fnotation.ma;h=62b8b2dcadd3a974d1b4749e633e03a385bf3236;hb=04cca085e96987e43b58f001bc8af317eb427ff2;hp=c698a5b12a658d6548592520c4077aff93bd7980;hpb=30f12b94fb7f9f201fb092a1b25a1c7e2f9b4564;p=helm.git

diff --git a/matita/matita/contribs/lambda/background/notation.ma b/matita/matita/contribs/lambda/background/notation.ma
index c698a5b12..62b8b2dca 100644
--- a/matita/matita/contribs/lambda/background/notation.ma
+++ b/matita/matita/contribs/lambda/background/notation.ma
@@ -14,6 +14,16 @@
 
 (* GENERIC NOTATION *********************************************************)
 
+(* Note: this should go to core_notation *)
+notation "⊥"
+  non associative with precedence 90
+  for @{'false}.
+
+(* Note: this should go to core_notation *)
+notation "⊤"
+  non associative with precedence 90
+  for @{'true}.
+
 (* Note: this should go to core_notation *)
 notation "hvbox(a break ≺ b)"
    non associative with precedence 45