From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 28 Feb 2021 21:32:01 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~153
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77c9255de3c5f7780aeacd745703a1cc76328a68;p=helm.git

update in ground

+ notation restyled
---

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc
index c829279fd..bb30f97e9 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc
@@ -1,5 +1,5 @@
 PccFor d "" true false
-GROUND NOTATION, GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ
+GROUND NOTATION
 RELATIONS
 FUNCTIONS
 LOGIC
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml
index 7fda12b7c..1adbf9894 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml
@@ -12,7 +12,6 @@ let step k st outs ins =
   | "FUNCTIONS" :: tl -> k T.OK ("FUNCTIONS" :: outs) tl
   | "RELATIONS" :: tl -> k T.OK ("RELATIONS" :: outs) tl
   | "GROUND" :: "NOTATION" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
-  | "GENERAL" :: "NOTATION" :: "USED" :: "BY" :: "THE" :: "FORMAL" :: "SYSTEM" :: "\206\187\206\180" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
   | _ -> k T.OO outs ins
 
 let main =
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma
index f6d95184b..acf8e6df2 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( l1 @@ break l2 )"
   right associative with precedence 47
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
index f770230c8..38d063225 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f @❨ break term 46 a ❩ )"
   non associative with precedence 60
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma
index 52ebf0ebd..fddd6406b 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐁❨ term 46 l, break term 46 h ❩ )"
   non associative with precedence 90
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma
index 53cf85698..669db2e7a 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( Ⓔ )"
-   non associative with precedence 55
-   for @{ 'CircledE $S }.
+  non associative with precedence 55
+  for @{ 'CircledE $S }.
 
 notation > "hvbox( Ⓔ )"
-   non associative with precedence 55
-   for @{ 'CircledE ? }.
+  non associative with precedence 55
+  for @{ 'CircledE ? }.
 
 notation > "hvbox( Ⓔ{ term 46 C } )"
-   non associative with precedence 55
-   for @{ 'CircledE $S }.
+  non associative with precedence 55
+  for @{ 'CircledE $S }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma
index 252f567bd..d633138cd 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f2 ~∘ break f1 )"
   right associative with precedence 60
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma
index 4f218dd61..8199b1429 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "◊"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma
index e35058c60..46000a861 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ↓ term 70 T )"
-   non associative with precedence 70
-   for @{ 'DownArrow $T }.
+  non associative with precedence 70
+  for @{ 'DownArrow $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma
index 3b7824afc..646685428 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( â«° term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoon $S $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoon $S $a }.
 
 notation > "hvbox( â«° term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoon ? $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoon ? $a }.
 
 notation > "hvbox( â«°{ term 46 S } break term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoon $S $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoon $S $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma
index c6ad562a3..0a57eea4e 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( â«°*[ break term 46 n ] break term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoonStar $S $n $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoonStar $S $n $a }.
 
 notation > "hvbox( â«°*[ break term 46 n ] break term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoonStar ? $n $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoonStar ? $n $a }.
 
 notation > "hvbox( â«°*{ term 46 S }[ break term 46 n ] break term 46 a )"
-   non associative with precedence 46
-   for @{ 'DownSpoonStar $S $n $a }.
+  non associative with precedence 46
+  for @{ 'DownSpoonStar $S $n $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma
index 7e82080a2..cb0d3c883 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ⫱ term 46 T )"
-   non associative with precedence 46
-   for @{ 'DropPred $T }.
+  non associative with precedence 46
+  for @{ 'DropPred $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma
index 90c206208..7336f0cd0 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ⫱ *[ term 46 n ] break term 46 T )"
-   non associative with precedence 46
-   for @{ 'DropPreds $n $T }.
+  non associative with precedence 46
+  for @{ 'DropPreds $n $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma
index 018bea05a..ea7f39835 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( f ^ break x )"
   left associative with precedence 75
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma
index 9d4aea574..97a04ef17 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐈𝐝 )"
-   non associative with precedence 90
-   for @{ 'Identity }.
+  non associative with precedence 90
+  for @{ 'Identity }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma
index f5c849158..8a6a2eba9 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "∞"
-   non associative with precedence 55
-   for @{ 'Infinity }.
+  non associative with precedence 55
+  for @{ 'Infinity }.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma
index af692211e..25e0d34cb 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "Ⓕ"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma
index 1a6b8474b..ba189fbb9 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟏"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma
index 5df776e6a..640ba879e 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟙𝟘"
-   non associative with precedence 55
-   for @{ 'OneZero }.
+  non associative with precedence 55
+  for @{ 'OneZero }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma
index e172f4abe..27d9b57ca 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( hd ⨮ break tl )"
   right associative with precedence 47
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma
index cd884bde6..ee874bc9f 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ❨ term 46 hd1, break term 46 hd2 ❩; break term 46 tl )"
   non associative with precedence 47
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma
index 551ee0d94..50b96096d 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox ( 〈 term 46 x1, break term 46 x2 , break term 46 x3, break term 46 x4 〉 )"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma
index 2562f0af7..1f770896c 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟐"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma
index df29e6b1a..ad7877afe 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐔 ❨ break term 46 a ❩ )"
   non associative with precedence 90
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma
index 1402237cd..cc3bb324b 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ↑ term 70 T )"
-   non associative with precedence 70
-   for @{ 'UpArrow $T }.
+  non associative with precedence 70
+  for @{ 'UpArrow $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma
index 50e07287a..899beb264 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ↑*[ term 46 n ] break term 70 T )"
-   non associative with precedence 70
-   for @{ 'UpArrowStar $n $T }.
+  non associative with precedence 70
+  for @{ 'UpArrowStar $n $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma
index 26ac82e66..47b35d5d9 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ↕* term 46 T )"
-   non associative with precedence 46
-   for @{ 'UpDownArrowStar $T }.
+  non associative with precedence 46
+  for @{ 'UpDownArrowStar $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma
index 2c71ef371..406f4a866 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ⫯ term 46 T )"
-   non associative with precedence 46
-   for @{ 'UpSpoon $T }.
+  non associative with precedence 46
+  for @{ 'UpSpoon $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma
index c9a1e3184..b3b50c643 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( ⫯*[ term 46 n ] break term 46 T )"
-   non associative with precedence 46
-   for @{ 'UpSpoonStar $n $T }.
+  non associative with precedence 46
+  for @{ 'UpSpoonStar $n $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma
index c321749ae..824475dcc 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "Ⓣ"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma
index 59b76ebb0..50f6bb0db 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟎"
   non associative with precedence 55
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma
index ff195abe1..a4fabaa47 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟘𝟙"
-   non associative with precedence 55
-   for @{ 'ZeroOne }.
+  non associative with precedence 55
+  for @{ 'ZeroOne }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma
index cb4b10dad..bf415b56a 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "𝟘𝟘"
-   non associative with precedence 55
-   for @{ 'ZeroZero }.
+  non associative with precedence 55
+  for @{ 'ZeroZero }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
index f3a39a720..ede24a0fe 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( f1 ≐ break term 46 f2 )"
-   non associative with precedence 45
-   for @{ 'DotEq $A $B $f1 $f2 }.
+  non associative with precedence 45
+  for @{ 'DotEq $A $B $f1 $f2 }.
 
 notation > "hvbox( f1 ≐ break term 46 f2 )"
-   non associative with precedence 45
-   for @{ 'DotEq ? ? $f1 $f2 }.
+  non associative with precedence 45
+  for @{ 'DotEq ? ? $f1 $f2 }.
 
 notation > "hvbox( f1 ≐{ break term 46 A, break term 46 B } break term 46 f2 )"
-   non associative with precedence 45
-   for @{ 'DotEq $A $B $f1 $f2 }.
+  non associative with precedence 45
+  for @{ 'DotEq $A $B $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
index be8260416..8ade3ee43 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f1 ≡ break term 46 f2 )"
-   non associative with precedence 45
-   for @{ 'IdEq $f1 $f2 }.
+  non associative with precedence 45
+  for @{ 'IdEq $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma
index 1a25c7878..398b4dfb8 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝛀❪ term 46 f ❫ )"
-   non associative with precedence 45
-   for @{ 'IsDivergent $f }.
+  non associative with precedence 45
+  for @{ 'IsDivergent $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma
index ac60a895b..a0bb366a2 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐅❪ term 46 f ❫ )"
-   non associative with precedence 45
-   for @{ 'IsFinite $f }.
+  non associative with precedence 45
+  for @{ 'IsFinite $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma
index 03fb76098..43fdded1b 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐈❪ term 46 f ❫ )"
-   non associative with precedence 45
-   for @{ 'IsIdentity $f }.
+  non associative with precedence 45
+  for @{ 'IsIdentity $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma
index e40a895ec..687c9e1d3 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐌❪ term 46 n, break term 46 c ❫ )"
-   non associative with precedence 45
-   for @{ 'IsM $n $c }.
+  non associative with precedence 45
+  for @{ 'IsM $n $c }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma
index 5b4420208..a0801cba7 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐓❪ term 46 f ❫ )"
-   non associative with precedence 45
-   for @{ 'IsT $f }.
+  non associative with precedence 45
+  for @{ 'IsT $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma
index e9a96facb..e337f5f29 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐓❪ term 46 n, break term 46 c ❫ )"
-   non associative with precedence 45
-   for @{ 'IsT $n $c }.
+  non associative with precedence 45
+  for @{ 'IsT $n $c }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma
index bc66e5c6d..e0f081ca3 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐔❪ term 46 f ❫ )"
-   non associative with precedence 45
-   for @{ 'IsUniform $f }.
+  non associative with precedence 45
+  for @{ 'IsUniform $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma
index dbbc88185..66c830c56 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f1 ∥ break term 46 f2 )"
-   non associative with precedence 45
-   for @{ 'Parallel $f1 $f2 }.
+  non associative with precedence 45
+  for @{ 'Parallel $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma
index c54b60b71..0f4bbd9e9 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f1 ⊚ break term 46 f2 ≘ break term 46 f )"
-   non associative with precedence 45
-   for @{ 'RAfter $f1 $f2 $f }.
+  non associative with precedence 45
+  for @{ 'RAfter $f1 $f2 $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma
index 007b7f1a4..63317f836 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( @❪ term 46 T1 , break term 46 f ❫ ≘ break term 46 T2 )"
-   non associative with precedence 45
-   for @{ 'RAt $T1 $f $T2 }.
+  non associative with precedence 45
+  for @{ 'RAt $T1 $f $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma
index 83fc39664..e3255ea92 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( f1 ~⊚ break term 46 f2 ≘ break term 46 f )"
-   non associative with precedence 45
-   for @{ 'RCoAfter $f1 $f2 $f }.
+  non associative with precedence 45
+  for @{ 'RCoAfter $f1 $f2 $f }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma
index 785c4cbc5..7a0a82148 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( 𝐂❪ term 46 f ❫ ≘ break term 46 n )"
-   non associative with precedence 45
-   for @{ 'RCoLength $f $n }.
+  non associative with precedence 45
+  for @{ 'RCoLength $f $n }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma
index e8ca369b7..1061fc073 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma
@@ -12,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( v1 ≗ break term 46 v2 )"
-   non associative with precedence 45
-   for @{ 'RingEq $M $v1 $v2 }.
+  non associative with precedence 45
+  for @{ 'RingEq $M $v1 $v2 }.
 
 notation > "hvbox( v1 ≗ break term 46 v2 )"
-   non associative with precedence 45
-   for @{ 'RingEq ? $v1 $v2 }.
+  non associative with precedence 45
+  for @{ 'RingEq ? $v1 $v2 }.
 
 notation > "hvbox( v1 ≗{ break term 46 M } break term 46 v2 )"
-   non associative with precedence 45
-   for @{ 'RingEq $M $v1 $v2 }.
+  non associative with precedence 45
+  for @{ 'RingEq $M $v1 $v2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma
index e7e93d23c..cd1bd316f 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( L1 ⋒ break term 46 L2 ≘ break term 46 L )"
-   non associative with precedence 45
-   for @{ 'RIntersection $L1 $L2 $L }.
+  non associative with precedence 45
+  for @{ 'RIntersection $L1 $L2 $L }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma
index 87177eb97..683919080 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( T1 ▭ break term 46 T2 ≘ break term 46 T )"
-   non associative with precedence 45
-   for @{ 'RMinus $T1 $T2 $T }.
+  non associative with precedence 45
+  for @{ 'RMinus $T1 $T2 $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma
index 54b036675..a289dc834 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "hvbox( L1 ⋓ break term 46 L2 ≘ break term 46 L )"
-   non associative with precedence 45
-   for @{ 'RUnion $L1 $L2 $L }.
+  non associative with precedence 45
+  for @{ 'RUnion $L1 $L2 $L }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma
index 854eb7b8c..5184bcd1a 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation > "hvbox(∧∧ term 34 P0 break & term 34 P1)"
- non associative with precedence 35
- for @{ 'and $P0 $P1 }.
+  non associative with precedence 35
+  for @{ 'and $P0 $P1 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma
index b96432510..56f2cda7a 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "⊥"
   non associative with precedence 19
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma
index c5da136f2..b10633313 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation > "hvbox(∨∨ term 29 P0 break | term 29 P1)"
- non associative with precedence 30
- for @{ 'or $P0 $P1 }.
+  non associative with precedence 30
+  for @{ 'or $P0 $P1 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma
index 7a9ad4366..055bdcf84 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+(* GROUND NOTATION **********************************************************)
 
 notation "⊤"
   non associative with precedence 19