X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnotation.ma;h=5e730aec23eb5a335e09e06dc256c88840fbbc12;hb=6d3e67a714d59ff5d0da7aff72323a6d2ac07db4;hp=9c9c19209357e58b563888a367fed8016b080207;hpb=28b55bc982671bad6514751c3a368b6cc6cbeec7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index 9c9c19209..5e730aec2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -252,6 +252,16 @@ notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'Unwind $L1 $T $L2 }.
 
+(* Restricted ***************************************************************)
+
+notation "hvbox( L ⊢ break term 46 T1 ➤ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRestStar $L $T1 $T2 }.
+
+notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRestStarSn $T1 $T2 }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )"