X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fbishop_set.ma;h=8cb77ec24289c633e6adcb535394156e0f053224;hb=89f78f0dcea3eabe47182bdb27bfca8a97cfc3e5;hp=9fee3d9fd3c0cdd3e640ee9054a84b89bf4d59ce;hpb=cb2419357a3f80388f71eb2730bff154bd4ef000;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index 9fee3d9fd..8cb77ec24 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -101,12 +101,12 @@ interpretation "bishop set subset" 'subset a b = (bs_subset _ a b).
 
 definition square_bishop_set : bishop_set → bishop_set.
 intro S; apply (mk_bishop_set (S × S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+[1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y));
 |2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
 |3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
 |4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
-    [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
-    |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+    [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption;
+    |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]]
 qed.
 
 notation "s 2 \atop \neq" non associative with precedence 90