]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
- new component "s_transition" for the restored fqu and fquq
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / notation / relations / dpredstar_7.ma
index ceb7aaf654dc4ca2b1779a76759b8ce8b5ff39fa..a85c0e4f890c3cc3a437814b4dc37f81d14b2a83 100644 (file)
@@ -16,4 +16,4 @@
 
 notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 o , break term 46 h , break term 46 n ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'DPRedStar $o $h $n $G $L $T1 $T2 }.
+   for @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }.