reorganization of the whole story, the root dir contains the algebraic structure

[helm.git] / matita / dama / ordered_groups.ma

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index a9912d43f55ccb92bd22ecec4c9e3320e68146ef..10e8f189ab0d4aeea549902fa4c2671372188f48 100644 (file)
--- a/matita/dama/ordered_groups.ma
+++ b/matita/dama/ordered_groups.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/ordered_groups/".
 
 include "groups.ma".
-include "ordered_sets2.ma".
+include "ordered_sets.ma".
 
 record pre_ordered_abelian_group : Type ≝
  { og_abelian_group:> abelian_group;