X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=e8ca08046d97164ea86bd987624231f01bb1940b;hb=41c4bfe9415b1b40278878dd767b734c61a47a69;hp=596424938e459fb0e62d51f5e8fd0bc5d13b475b;hpb=6e7aeeede341ed115191782ca597abf0ffc86564;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 596424938..e8ca08046 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -92,3 +92,7 @@ notation "hvbox(《T》 break _ [E])"
 notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
+
+notation "hvbox(𝕂{T} break _ [E])"
+   non associative with precedence 50
+   for @{'IK1 $T $E}.