X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Fre.ma;h=234d522ae176dde98579f39ac9e6ac09bb11aa32;hb=64a752136a679bcab14a9cd01823c18b7cc991de;hp=af0e921a6b9a1be5cbabe311860e2fb8d7d09c8b;hpb=fe7d9f4665e92d9c6934988b2b215547ab7ecf3f;p=helm.git

diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index af0e921a6..234d522ae 100644
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -128,8 +128,7 @@ let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
   | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
   | pk E ⇒ (forget ? E)^* ].
  
-(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
-interpretation "forget" 'norm a = (forget ? a).
+interpretation "forget" 'card a = (forget ? a).
 
 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
 // qed.