X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Ffields.ma;h=305c49764e9b651f368171ce00db323b29568956;hb=f79585fe2f19c4a545938e189439d87b2611a47a;hp=2aac4f446faa08237fe5ca25265e51630de0b147;hpb=d61b0ec37e7943a058dc9c6381efe49db7eb575f;p=helm.git

diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/fields.ma
index 2aac4f446..305c49764 100644
--- a/helm/software/matita/dama/fields.ma
+++ b/helm/software/matita/dama/fields.ma
@@ -55,5 +55,6 @@ theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1.
  apply (inv_inverse_ ? ? (field_properties F)).
 qed.
 
+(*CSC: qua funzionava anche mettendo ? al posto della prima F*)
 definition sum_field ≝
- λF:field. sum ? (plus F) 0 1.
+ λF:field. sum F (plus F) 0 1.