From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 17:35:24 +0000 (+0000) Subject: The precedence of ^-1 has changed. X-Git-Tag: make_still_working~2968 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b960f999600fc7e1037a08c700e50336c96db755;p=helm.git The precedence of ^-1 has changed. From: sacerdot --- diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma index 54e920c2e..40b2f72bb 100644 --- a/helm/software/matita/nlibrary/overlap/o-algebra.ma +++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma @@ -220,7 +220,7 @@ nlemma ORelation_eq2: r=r' → r⎻ = r'⎻. #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx); napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_ - [ napply e | napply e^-1] + [ napply e | napply (e^-1)] nqed. ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) @@ -259,7 +259,7 @@ nlemma ORelation_eq3: r=r' → r* = r'*. #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx); napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_ - [ napply e | napply e^-1] + [ napply e | napply (e^-1)] nqed. ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q) @@ -295,7 +295,7 @@ nlemma ORelation_eq4: r=r' → r⎻* = r'⎻*. #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx); napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_ - [ napply e | napply e^-1] + [ napply e | napply (e^-1)] nqed. ndefinition or_f_minus_star_morphism1: