X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=0ad437ab04ba21c70ae70fa78314c80e3acf5dd2;hb=60779bad5c038c5573514800a7b50eafb45013fa;hp=42f3eb2aa7c3742ae656ddaa9a29bee39962378e;hpb=060f4ff9bcece134dd66757ee7f8c571bdbc8cab;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 42f3eb2aa..0ad437ab0 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -20,22 +20,38 @@ notation "hvbox(a break ≅ b)"
   non associative with precedence 45
   for @{'Eq $a $b}.
 
+notation "hvbox(a break (≅ ^ term 90 c) b)"
+  non associative with precedence 45
+  for @{'Eq1 $c $a $b}.
+
 (* lifting, substitution *)
 
 notation "hvbox(M break [ l ])"
    non associative with precedence 90
    for @{'Subst1 $M $l}.
 
-(* evaluation, interpretation *)
+(* interpretation *)
 
 notation "hvbox(〚term 90 T〛)"
    non associative with precedence 50
-   for @{'Eval $T}.
+   for @{'IInt $T}.
 
 notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
    non associative with precedence 50
-   for @{'Eval1 $T $E}.
+   for @{'IInt1 $T $E}.
 
 notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
    non associative with precedence 50
-   for @{'Eval2 $T $E1 $E2}.
+   for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(《term 90 T》)"
+   non associative with precedence 50
+   for @{'EInt $T}.
+
+notation "hvbox(《term 90 T》 break _ [term 90 E])"
+   non associative with precedence 50
+   for @{'EInt1 $T $E}.
+
+notation "hvbox(《term 90 T》 break _ [term 90 E1 break , term 90 E2])"
+   non associative with precedence 50
+   for @{'EInt2 $T $E1 $E2}.