X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter7.ma;h=20b670018cc21de67fb8227e53ebe4cca692984e;hb=cbbbc763dc971b43fe74f1d08b797de5d1dc4f17;hp=4b12b75fcf1c682779bebe3c8ecb2d7e560a5f6c;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter7.ma b/matita/matita/lib/tutorial/chapter7.ma
index 4b12b75fc..20b670018 100644
--- a/matita/matita/lib/tutorial/chapter7.ma
+++ b/matita/matita/lib/tutorial/chapter7.ma
@@ -120,9 +120,11 @@ let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
   | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
   | 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).
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
+interpretation "forget" 'card a = (forget ? a).
 
 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
 // qed.
@@ -305,4 +307,4 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
   |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
   ]
-qed.
\ No newline at end of file
+qed.