- untranslated sections of "formal_topology" commented to make it compile

[helm.git] / matita / matita / lib / tutorial / chapter7.ma

diff --git a/matita/matita/lib/tutorial/chapter7.ma b/matita/matita/lib/tutorial/chapter7.ma
index 4b12b75fcf1c682779bebe3c8ecb2d7e560a5f6c..739afb52df7acd0ad2af9e964f98ce0fc4568daf 100644 (file)
--- a/matita/matita/lib/tutorial/chapter7.ma
+++ b/matita/matita/lib/tutorial/chapter7.ma
@@ -121,8 +121,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.