]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/dama/attic/ordered_fields_ch0.ma
cleanup of the eq_trans burdain
[helm.git] / helm / software / matita / dama / attic / ordered_fields_ch0.ma
index b312c31ab6f43f7f8ea57484397b067dbc6c5206..5be3c9da49eaea573feb1723c19d33f9635f1ca3 100644 (file)
@@ -18,7 +18,7 @@ include "attic/fields.ma".
 include "ordered_group.ma".
 
 (*CSC: non capisco questi alias! Una volta non servivano*)
-alias id "plus" = "cic:/matita/groups/plus.con".
+alias id "plus" = "cic:/matita/group/plus.con".
 alias symbol "plus" = "Abelian group plus".
 
 record pre_ordered_field_ch0: Type ≝