From b960f999600fc7e1037a08c700e50336c96db755 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 17:35:24 +0000 Subject: [PATCH] The precedence of ^-1 has changed. From: sacerdot --- helm/software/matita/nlibrary/overlap/o-algebra.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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: -- 2.39.2