- some renaming

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lpc / lfpc.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
index 273873abdcf64a8142ec43b93603b80613988f04..b80b290b63a3c09b3ecc0b6c7440b1d4b551ca00 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpc/lfpc.etc
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ break ⦃ term 46 L2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
 include "basic_2/reducibility/lfpr.ma".
 
 (* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)