Porting of Sambin's stuff started.

[helm.git] / helm / software / matita / nlibrary / topology / igft-setoid.ma

diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma
index 30f2d161ee21296d76af768993e537e6c62b64ba..7235b4ba08bb164a12dc616f110aaaf8ad1a76c9 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft-setoid.ma
+++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma
@@ -200,7 +200,7 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝
                 @; #w; #Hw; nwhd;
                 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);                    
                   
-    
+(*    
   
 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
@@ -574,3 +574,4 @@ D*)
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
 
 D*)
+*)
\ No newline at end of file