decentralizing core notation continues ...

+ apart, napart decentralized

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index 3bf1de3b26415caaaa7f52883e477eeeeb1a660c..4d1e355a304d695725cbfe62530607f886fcd2b7 100644 (file)
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -280,12 +280,6 @@ for @{ 'union $a $b }. (* \cup *)
 
 (* other notations **********************************************************)
 
-notation "hvbox(a break \approx b)" non associative with precedence 45 
-  for @{ 'napart $a $b}.
-        
-notation "hvbox(a break # b)" non associative with precedence 45 
-  for @{ 'apart $a $b}.
-
 notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
 notation > "a ^ term 90 b"  non associative with precedence 75 for @{ 'exp $a $b}.

diff --git a/matita/matita/lib/basics/core_notation/apart_2.ma b/matita/matita/lib/basics/core_notation/apart_2.ma
new file mode 100644 (file)
index 0000000..04c81ec
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/apart_2.ma
@@ -0,0 +1,15 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "hvbox(a break # b)" non associative with precedence 45 
+  for @{ 'apart $a $b}.

diff --git a/matita/matita/lib/basics/core_notation/napart_2.ma b/matita/matita/lib/basics/core_notation/napart_2.ma
new file mode 100644 (file)
index 0000000..a381787
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/napart_2.ma
@@ -0,0 +1,15 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "hvbox(a break \approx b)" non associative with precedence 45 
+  for @{ 'napart $a $b}.

diff --git a/matita/matita/lib/pts_dummy/rc_eval.ma b/matita/matita/lib/pts_dummy/rc_eval.ma
index 87cfd11dce28096d66b5f439ec5641300468cdeb..439160a7d0bc0b6315b76216a541325939f95923 100644 (file)
--- a/matita/matita/lib/pts_dummy/rc_eval.ma
+++ b/matita/matita/lib/pts_dummy/rc_eval.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "pts_dummy/rc_hsat.ma".
+include "basics/core_notation/napart_2.ma".
 (*
 (* THE EVALUATION *************************************************************)
 

diff --git a/matita/matita/lib/pts_dummy_new/rc_eval.ma b/matita/matita/lib/pts_dummy_new/rc_eval.ma
index 7b7ce54d983447cdbaf9cb3941acb4215ca3e7ea..c11eca57a8703489c1a23661b8f40261511443f4 100644 (file)
--- a/matita/matita/lib/pts_dummy_new/rc_eval.ma
+++ b/matita/matita/lib/pts_dummy_new/rc_eval.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "pts_dummy/rc_hsat.ma".
+include "basics/core_notation/napart_2.ma".
 (*
 (* THE EVALUATION *************************************************************)
 

diff --git a/matita/matita/lib/reverse_complexity/speed_clean.ma b/matita/matita/lib/reverse_complexity/speed_clean.ma
index 9b9fecf949282e3f167c00e6ec640871f95d0904..bfd3d34b150a1e6cdc0a7dce299d1989def3239b 100644 (file)
--- a/matita/matita/lib/reverse_complexity/speed_clean.ma
+++ b/matita/matita/lib/reverse_complexity/speed_clean.ma
@@ -4,6 +4,7 @@ include "arithmetics/bigops.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 
@@ -1064,4 +1065,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
-  
\ No newline at end of file
+  

diff --git a/matita/matita/lib/reverse_complexity/speed_def.ma b/matita/matita/lib/reverse_complexity/speed_def.ma
index 6a0ec4a57a82f23fc26dd4bbb8c90f1927e99b05..9812cfb08673852fa2f7736c6ead07857a9d95dc 100644 (file)
--- a/matita/matita/lib/reverse_complexity/speed_def.ma
+++ b/matita/matita/lib/reverse_complexity/speed_def.ma
@@ -4,6 +4,7 @@ include "arithmetics/bigops.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 
@@ -918,4 +919,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
-  
\ No newline at end of file
+  

diff --git a/matita/matita/lib/reverse_complexity/speed_new.ma b/matita/matita/lib/reverse_complexity/speed_new.ma
index 6a0ec4a57a82f23fc26dd4bbb8c90f1927e99b05..9812cfb08673852fa2f7736c6ead07857a9d95dc 100644 (file)
--- a/matita/matita/lib/reverse_complexity/speed_new.ma
+++ b/matita/matita/lib/reverse_complexity/speed_new.ma
@@ -4,6 +4,7 @@ include "arithmetics/bigops.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 
@@ -918,4 +919,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
-  
\ No newline at end of file
+  

diff --git a/matita/matita/lib/reverse_complexity/toolkit.ma b/matita/matita/lib/reverse_complexity/toolkit.ma
index 11f988c79dc29135397bd4931c3dc862ad861f53..69fa3525ab30ba2977b2affb92d5df3064287f5e 100644 (file)
--- a/matita/matita/lib/reverse_complexity/toolkit.ma
+++ b/matita/matita/lib/reverse_complexity/toolkit.ma
@@ -4,6 +4,7 @@ include "arithmetics/bigops.ma".
 include "arithmetics/sigma_pi.ma".
 include "arithmetics/bounded_quantifiers.ma".
 include "reverse_complexity/big_O.ma".
+include "basics/core_notation/napart_2.ma".
 
 (************************* notation for minimization *****************************)
 notation "μ_{ ident i < n } p" 
@@ -984,4 +985,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg
   @Hmono @(mono_h_of2 … Hr Hmono … ltin)
  ]
 qed.
-  
\ No newline at end of file
+