basics: some additions

[helm.git] / matita / matita / lib / lambda / lambda_notation.ma

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 596424938e459fb0e62d51f5e8fd0bc5d13b475b..4f2f4f1dc5334a5308fc7e96bcef2a896d165b61 100644 (file)
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -69,6 +69,10 @@ notation "hvbox(║T║ break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'IInt2 $T $E1 $E2}.
 
+notation "hvbox(║T║ * break _ [E])"
+   non associative with precedence 50
+   for @{'IIntS1 $T $E}.
+
 notation "hvbox(〚T〛)"
    non associative with precedence 50
    for @{'EInt $T}.
@@ -92,3 +96,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}.