X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_tls.ma;h=d15047b0c63783a7bd033af33eff400b9a832998;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hp=e6134e7f9a77899840332443c91e06f67bed89d4;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
index e6134e7f9..d15047b0c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
@@ -12,33 +12,33 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/droppreds_2.ma".
+include "ground/notation/functions/downspoonstar_2.ma".
 include "ground/lib/stream_tls.ma".
 include "ground/relocation/gr_tl.ma".
 
 (* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
 (*** tls *)
-definition gr_tls (n) (f:gr_map) ≝ ⫰*[n]f.
+definition gr_tls (n) (f:gr_map) ≝ ⇣*[n]f.
 
 interpretation
   "iterated tail (generic relocation maps)"
-  'DropPreds n f = (gr_tls n f).
+  'DownSpoonStar n f = (gr_tls n f).
 
 (* Basic constructions (specific) *******************************************)
 
 (*** tls_O *)
-lemma gr_tls_zero (f): f = ⫱*[𝟎] f.
+lemma gr_tls_zero (f): f = ⫰*[𝟎] f.
 // qed.
 
 (*** tls_swap *)
-lemma gr_tls_tl (n) (f): ⫱⫱*[n] f = ⫱*[n] ⫱f.
+lemma gr_tls_tl (n) (f): â«°â«°*[n] f = â«°*[n] â«°f.
 /2 width=1 by stream_tls_tl/ qed.
 
 (*** tls_S *)
-lemma gr_tls_succ (n) (f): ⫱⫱*[n] f = ⫱*[↑n] f.
+lemma gr_tls_succ (n) (f): ⫰⫰*[n] f = ⫰*[↑n] f.
 /2 width=1 by stream_tls_succ/ qed.
 
 (*** tls_xn *)
-lemma gr_tls_swap (n) (f): ⫱*[n] ⫱f = ⫱*[↑n] f.
+lemma gr_tls_swap (n) (f): ⫰*[n] ⫰f = ⫰*[↑n] f.
 // qed.