]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma
- some renaming according to the written version of basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / notation / relations / freestar_4.ma
index 4ce6d2dc78daa9d941beeb141c1ca18e2acb30b1..e464806396a1b8a4a986d6cd3e23d9cea2f5643c 100644 (file)
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L ⊢ break term 46 i ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )"
+notation "hvbox( L ⊢ break term 46 i ϵ 𝐅 * [ break term 46 l ] ⦃ break term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'FreeStar $L $i $d $T }.
+   for @{ 'FreeStar $L $i $l $T }.