middot notation

[helm.git] / matita / matita / lib / turing / mono.ma

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 8ac1072268c75fba6f055fe1f6d458e446bfb6fc..e117fc7be167bf4bb034fc0d4c84d06ca31ee2dc 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -342,7 +342,7 @@ definition seq ≝ λsig. λM1,M2 : TM sig.
     (λs.match s with 
       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]). 
 
-notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
+notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "sequential composition" 'middot a b = (seq ? a b).
 
 definition lift_confL ≝