From c4c23fb49f67e69b3193fc8233339f6ca016a8e9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 24 May 2016 19:05:12 +0000 Subject: [PATCH] more files missing :(( --- .../lambdadelta/basic_2/notation/relations/predsn_5.ma | 4 ++-- .../basic_2/notation/relations/{predsn_3.ma => predtysn_5.ma} | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predsn_3.ma => predtysn_5.ma} (87%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma index 8c49c6b19..e1f79764c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 T ] break term 46 L2 )" non associative with precedence 45 - for @{ 'PRedSn $h $o $G $L1 $L2 }. + for @{ 'PRedSn $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma index d06064a29..8f82a99b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ break [ term 46 h , break term 46 T ] break term 46 L2 )" non associative with precedence 45 - for @{ 'PRedSn $G $L1 $L2 }. + for @{ 'PRedTySn $h $T $G $L1 $L2 }. -- 2.39.2