notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / streams_hdtl.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index 3a31efc350da7ba6e6769ce360969ddfa754b564..c8545966471fa12583d4b07c691de991018ad679 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/notation/functions/downspoon_1.ma".
 include "ground_2/lib/streams_eq.ma".
 include "ground_2/lib/arith.ma".
 
@@ -24,7 +24,7 @@ definition hd (A:Type[0]): stream A → A ≝
 definition tl (A:Type[0]): stream A → stream A ≝
               λt. match t with [ seq _ t ⇒ t ].
 
-interpretation "tail (streams)" 'Drop t = (tl ? t).
+interpretation "tail (streams)" 'DownSpoon t = (tl ? t).
 
 (* basic properties *********************************************************)
 
@@ -34,6 +34,6 @@ lemma hd_rew (A) (a) (t): a = hd A (a@t).
 lemma tl_rew (A) (a) (t): t = tl A (a@t).
 // qed.
 
-lemma eq_stream_split (A) (t): (hd â\80¦ t) @ â\86\93t â\89\90â¦\8bAâ¦\8c t.
+lemma eq_stream_split (A) (t): (hd â\80¦ t) @ â«°t â\89\97{A} t.
 #A * //
 qed.