]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/algebra/monoids.ma
nasty change in the lexer/parser:
[helm.git] / helm / software / matita / library / algebra / monoids.ma
index fe35eeb6709fea8092269d6035f470f6136c9523..9fc13f91e958bd46b730dbaf333884651e3f87e3 100644 (file)
@@ -32,7 +32,7 @@ record Monoid : Type ≝
    monoid_properties:> isMonoid premonoid 
  }.
 
-interpretation "Monoid unit" 'neutral = (e _).
+interpretation "Monoid unit" 'neutral = (e ?).
   
 definition is_left_inverse ≝
  λM:Monoid.