X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=8063634d0a3210410d4c98ed31b1dcfae41bb3dd;hb=2912d9bd61bc451c1135ca0a123cc30f203e93c9;hp=a5fb014ed7d284cc6cc493bd969c351baa297ef6;hpb=ffbc6cd1358d61072105766052c7498a1f37c769;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index a5fb014ed..8063634d0 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
-
+(* NOTATION FOR THE LAMBDA CALCULUS *)
 (* equivalence, invariance *)
 
 notation "hvbox(a break ≅ b)" 
@@ -70,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}.
@@ -93,3 +96,11 @@ notation "hvbox(《T》 break _ [E])"
 notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
+
+notation "hvbox(𝕂{G})"
+   non associative with precedence 50
+   for @{'IK $G}.
+
+notation "hvbox(𝕂{T} break _ [G])"
+   non associative with precedence 50
+   for @{'IK $T $G}.