X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Ftm.ma;h=f56ff538b764d322ec4431861f59e14c98b76e08;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=96a98fc75cd7c905ae3730ff34d5b591f86991c9;hpb=b5507c449ba38a76666a35664f9cf4e1953ad8ec;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
index 96a98fc75..f56ff538b 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
@@ -28,7 +28,7 @@ definition tm_co (p) (V) (T) ≝ ⓓ[p]V.(↑[1]T).
 
 definition tm_ap (V) (T) ≝ ⓐV.T.
 
-definition tm_ti (gv) (lv) (T) ≝ ●[gv,lv]T.
+definition tm_ti (gv) (lv) (T) ≝ ■[gv,lv]T.
 
 definition TM (h): model ≝ mk_model … .
 [ @tm_dd