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 c829279fd9ae01ba6947b43a4ffce40d2b1731e1..bb30f97e93f2bd8443b7e5465aaba31ed1b2d0fa 100644 (file)
--- 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 7fda12b7c4d94819341b339fad2269190699371e..1adbf98945473ecf02e4a7d6c42483591528df4c 100644 (file)
--- 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 f6d95184b79adab824bf849cd158735ad28a8a72..acf8e6df289cd08f6f4984780ad9a491473d7a8f 100644 (file)
--- 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 f770230c81ce0e9ac0b175cb53e0147d48bfa519..38d0632259779f191a4a3006f88e6de45a5e01ce 100644 (file)
--- 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 52ebf0ebdfe4f1f7918b0640ae35178dbbfce824..fddd6406b577353c16297ce7fefe9ad2ba4cdd24 100644 (file)
--- 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 53cf856984e4fba058b032eff98281cd5c74d28b..669db2e7aaea6f11a95f09f03d3609074e55233c 100644 (file)
--- 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 252f567bd0e2f5e8c086357ea3faf7cd002b2c1c..d633138cd2b9c8080cc72e6093c5d7c4d9275945 100644 (file)
--- 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 4f218dd6148795da24d17e51557a497a856dcb7c..8199b1429a9a14e08fef205d5bad07413ea35d0a 100644 (file)
--- 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 e35058c60b0244dce44d2e54bcbc82612ec8b053..46000a861ec025bbe941689ee00459bd540c044b 100644 (file)
--- 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 3b7824afcc77bc21853e395a1fee06b69f1e1ea2..64668542863b9c03a5abd0717d75f0dbd4af05ad 100644 (file)
--- 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 c6ad562a399081db256fdfb016207bca2f7335e0..0a57eea4eb4400bbb4f618e3e424321965fb463f 100644 (file)
--- 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 7e82080a27b110780cb1260cf2de451a160e0cbc..cb0d3c883449cdc1046106d47ea80a1747cb66e6 100644 (file)
--- 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 90c206208259aeefa3037063d447f50bc1c0107d..7336f0cd0ac85f77f4e0695a4baf297949187ae5 100644 (file)
--- 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 018bea05a60f6e5befb0b386def368b2f290d2e4..ea7f39835ee8d8250950bac4d0600a32c33d5a96 100644 (file)
--- 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 9d4aea574db3383c2f5574c8d1df296bb35efd15..97a04ef17c0e2bf88f87a66f0dc9b82409153135 100644 (file)
--- 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 f5c84915864f01f25e795e8a82cb4d6815eb69ea..8a6a2eba9c26f23ee430861998c972ad202fefae 100644 (file)
--- 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 af692211e458f4182c7d7b3931940476e95665b0..25e0d34cbe0085650f997638b00f7809d5fde6b7 100644 (file)
--- 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 1a6b8474b176023c0b817a0551278c3452ab82d1..ba189fbb9da14a645c1ac9a7c22635b3b22694b6 100644 (file)
--- 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 5df776e6a0b17c6a124f838cdfad99a2e4b9dc13..640ba879e3308b9c81916f3dd38b1063d21f3d37 100644 (file)
--- 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 e172f4abe8ac4de6a29f6b41bcd4d72afed69baa..27d9b57ca249011243397b4cfdf339957f8571ca 100644 (file)
--- 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 cd884bde6873d68c408bf6e8f2df8d3c45da1239..ee874bc9f094fbff6d322751089a4e0d53bdb28b 100644 (file)
--- 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 551ee0d949a2846ca9861bebbcb2ec7f85305441..50b96096da12b2515212cd31884e8186f53dc1c5 100644 (file)
--- 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 2562f0af702105bccbe3370a2e368642847b9f95..1f770896c7ac11ee312dc66554afd8915339bae7 100644 (file)
--- 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 df29e6b1a50d26ff9fe2225322be33333fa566dc..ad7877afee27542e6e45135bf8f475521d8c499e 100644 (file)
--- 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 1402237cd2c10a501ac8dd1fb2156dd4ac7966e8..cc3bb324bfdac91bb8ecf4b1ffc5fe5584346956 100644 (file)
--- 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 50e07287a92c739c9edcd6102430c33bab9d9908..899beb26458789f3c213f578eb39d6dc46dd9b75 100644 (file)
--- 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 26ac82e66f70d2e16f3b1c586330d13da4361c4e..47b35d5d971fe1edebf6e49065b4254671c65605 100644 (file)
--- 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 2c71ef371930f73d3cf5d281ac069ec1731d6374..406f4a8664f806a7872d657bab6c02efa0e55ad5 100644 (file)
--- 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 c9a1e3184fc837a051498b4f13d9a680d115893a..b3b50c6437124a8fc45c7986979a128e3208f256 100644 (file)
--- 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 c321749ae34d79065a03bcc85a9e09e12ca22135..824475dcc8b448c1a028119dfdcd38dffe88e41d 100644 (file)
--- 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 59b76ebb0cdad889e4d67a37c3a1d5d104872c02..50f6bb0dbcf4079dfbf1262daaf514148905a17f 100644 (file)
--- 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 ff195abe1ab34025bce4dec87c422ad3610a869e..a4fabaa474e386b18596cea7df97cfdd4ed8d2c5 100644 (file)
--- 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 cb4b10dad6736f53419a877db55e52af1fa202dc..bf415b56afffbac0a487522bb76e2f5be068c853 100644 (file)
--- 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 f3a39a72026586edcdfecfe25779cbfd496dfe4a..ede24a0fee7741a97676b6db57c7adc0e494c2f7 100644 (file)
--- 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 be826041636f8e27d1394b46fff1afeff516af5e..8ade3ee431d663a7d29f628851ac64bbd48a4016 100644 (file)
--- 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 1a25c7878c4c2801afb8b4670587003d366d659a..398b4dfb8389a62f9b16b92d14342ca137d1ac9b 100644 (file)
--- 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 ac60a895b315103456caa46f957cf2cb16f68381..a0bb366a2066ace6944454121ec5e46787c26c3f 100644 (file)
--- 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 03fb76098af8a376c60a2f4471548745692c9945..43fdded1bf24eda7c541d19f4bb74bc2d71606a2 100644 (file)
--- 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 e40a895ec4d9ae57b475a1469a4dc835e714de7d..687c9e1d36ca5d58216aa574512ccc7ff103b266 100644 (file)
--- 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 5b4420208929b9bab9d6955d4e08c8c241b04424..a0801cba74b79e2d4fc009415ede1ce37067c7e4 100644 (file)
--- 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 e9a96facbe99fade9711d7e5ff5e56db771a9567..e337f5f290956cb4907964e1da6ef3f79754c899 100644 (file)
--- 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 bc66e5c6d7d21688ea35cee81ed889782283d132..e0f081ca36c6adcf01e00b77db450bcb9e7f6bbd 100644 (file)
--- 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 dbbc88185ae6da78406f0293820ad3efa9d2d2a8..66c830c56e8bbda4478a2926358d7478e04ea901 100644 (file)
--- 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 c54b60b71f5e5b86eefd36521eb1fb3682690ae4..0f4bbd9e908a9dc338c65a3cee19c8cc61c773cf 100644 (file)
--- 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 007b7f1a4445ce2a909f7a60c87761d3227bb78e..63317f836a44bc65aa2c5d986c8cf973093d31f2 100644 (file)
--- 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 83fc39664d2782309d68aa3c69ae14ba1604fda2..e3255ea92dec6d04354d48c9d32d0b4c0fd6d48b 100644 (file)
--- 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 785c4cbc5d419b1852e150fdccaefd36c5381243..7a0a82148a8236e827e7f407c321a6539b9ddb1d 100644 (file)
--- 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 e8ca369b7b8feb7b437f24de34e0ba67129e2499..1061fc0731efb4ad1a2b231c62d679fda262f656 100644 (file)
--- 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 e7e93d23c127864c95ed72de8846fe34beffac9a..cd1bd316f0981a7790d3ad37034268a1249a51f8 100644 (file)
--- 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 87177eb976c93e3ce00c2c3343ec610a607e839b..6839190808353cc41b438b16e482890b8b1d659e 100644 (file)
--- 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 54b03667556a45a5d6987dbe5a8cc1363e0042de..a289dc8344e422266277ea70714b42803e112ee9 100644 (file)
--- 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 854eb7b8c1512065d6eaf485040e33b20e43f28c..5184bcd1a350c193af297de1bfa30e974bda75c7 100644 (file)
--- 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 b96432510654ab11eb9a22d97579609cf121d034..56f2cda7af7a78034273e8bc2350875e45982d2f 100644 (file)
--- 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 c5da136f2944633bb7a2b9cd1e8316a2c7d2a32b..b106333133ea5972b3613a8e17f1b6fb3ca7a29b 100644 (file)
--- 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 7a9ad4366f21d77528d261801cf540e091d62c1e..055bdcf84bbef4e2f64616a4512512a247493979 100644 (file)
--- 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