]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/dama/bishop_set.ma
dama almost ok
[helm.git] / helm / software / matita / library / dama / bishop_set.ma
index d69bb2732b3f1a4a023aa21bdd54fc4635c3b7b7..3fa4eda96910abbabd26842e13d948c23706d1e6 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
+include "dama/ordered_set.ma".
 
 (* Definition 2.2, setoid *)
 record bishop_set: Type ≝ {
@@ -86,4 +86,4 @@ notation "s 2 \atop \neq" non associative with precedence 90
 notation > "s 'squareB'" non associative with precedence 90
   for @{ 'squareB $s }.
 interpretation "bishop set square" 'squareB x = (square_bishop_set x).
-interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).