update in lib

+ notation for card decentralized

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index 54bfd22d512e7917f7102f9c5f7ee165f2695e0c..52ca7e961a499ddc7d4d36bc4898a038696a2b16 100644 (file)
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -277,8 +277,6 @@ for @{ 'union $a $b }. (* \cup *)
 
 (* other notations **********************************************************)
 
-notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
-
 notation "\naturals" non associative with precedence 90 for @{'N}.
 notation "\rationals" non associative with precedence 90 for @{'Q}.
 notation "\reals" non associative with precedence 90 for @{'R}.

diff --git a/matita/matita/lib/basics/core_notation/card_1.ma b/matita/matita/lib/basics/core_notation/card_1.ma
new file mode 100644 (file)
index 0000000..2324935
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/card_1.ma
@@ -0,0 +1,14 @@
+(*
+    ||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 "| term 19 C |" with precedence 70 for @{ 'card $C }.

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index f8c2ac772084c11ba0e0dd273f9676f3ce3d46f5..ed988b760d283732144e949e2b8c189b4df46283 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -11,6 +11,7 @@
 
 include "basics/types.ma".
 include "arithmetics/nat.ma".
+include "basics/core_notation/card_1.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A

diff --git a/matita/matita/lib/hott/notations.ma b/matita/matita/lib/hott/notations.ma
index 09a8c37cc7dcd9cb69118b69ccf2b047368e9eec..d680e4bd1c0f7d011774f5a7803655220775a106 100644 (file)
--- a/matita/matita/lib/hott/notations.ma
+++ b/matita/matita/lib/hott/notations.ma
@@ -302,8 +302,6 @@ notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
 (*
 notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. 
 
-notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
-
 notation "\naturals" non associative with precedence 90 for @{'N}.
 notation "\rationals" non associative with precedence 90 for @{'Q}.
 notation "\reals" non associative with precedence 90 for @{'R}.

diff --git a/matita/matita/lib/lambda/paths/decomposed_trace.ma b/matita/matita/lib/lambda/paths/decomposed_trace.ma
index 9c391c1a9afba303a4177b789c77013301ba32d5..1e6ae78de2a3a9a0f06fbaa495ea1f9545bfb05d 100644 (file)
--- a/matita/matita/lib/lambda/paths/decomposed_trace.ma
+++ b/matita/matita/lib/lambda/paths/decomposed_trace.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "lambda/paths/trace.ma".
+include "basics/core_notation/card_1.ma".
 
 (* DECOMPOSED TRACE *********************************************************)
 

diff --git a/matita/matita/lib/lambda/terms/size.ma b/matita/matita/lib/lambda/terms/size.ma
index 3396dc415044f7a1f596ddc86b439350e60efdf5..a07112701dd5b235c8368b02440518284d6a0427 100644 (file)
--- a/matita/matita/lib/lambda/terms/size.ma
+++ b/matita/matita/lib/lambda/terms/size.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "lambda/terms/relocation.ma".
+include "basics/core_notation/card_1.ma".
 
 (* SIZE *********************************************************************)
 

diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index 234d522ae176dde98579f39ac9e6ac09bb11aa32..8ba714b82592f01047735b685663a64ed200f3d5 100644 (file)
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "re/lang.ma".
+include "basics/core_notation/card_1.ma".
 
 (* The type re of regular expressions over an alphabet $S$ is the smallest 
 collection of objects generated by the following constructors: *)

diff --git a/matita/matita/lib/reverse_complexity/hierarchy.ma b/matita/matita/lib/reverse_complexity/hierarchy.ma
index d833a5164e2949d119e1ffeb2d4b471b4fbaf6f6..cae93c2560172486e10ba8d11c8c135a1c46098b 100644 (file)
--- a/matita/matita/lib/reverse_complexity/hierarchy.ma
+++ b/matita/matita/lib/reverse_complexity/hierarchy.ma
@@ -6,6 +6,7 @@ include "arithmetics/bounded_quantifiers.ma".
 include "arithmetics/pidgeon_hole.ma". 
 include "basics/sets.ma".
 include "basics/types.ma".
+include "basics/core_notation/card_1.ma".
 
 (************************************ MAX *************************************)
 notation "Max_{ ident i < n | p } f"
@@ -468,4 +469,4 @@ cut (O (λx:ℕ.sU x x (s x)) s) [%{1} %{0} #n //]
   |%{1} %{0} #n #_ >commutative_times <times_n_1
    @monotonic_sU // >size_f_size >size_of_size //
   ]
-qed.
\ No newline at end of file
+qed.

diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma
index 21a8abd2fcc515d169a2dca0335ab3136497da8f..b1493982ce9fea0bc002020a84c733e766454dc8 100644 (file)
--- a/matita/matita/lib/tutorial/chapter5.ma
+++ b/matita/matita/lib/tutorial/chapter5.ma
@@ -4,7 +4,7 @@
 
 include "tutorial/chapter4.ma".
 include "arithmetics/nat.ma".
-
+include "basics/core_notation/card_1.ma".
 
 (******************************** Option Type *********************************)
 

diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma
index 427b148427f3e34efde54a55286a284424c0b1be..47cfbdeb7b392e6539c1ff877898334142e64fe4 100644 (file)
--- a/matita/matita/lib/tutorial/chapter8.ma
+++ b/matita/matita/lib/tutorial/chapter8.ma
@@ -5,6 +5,7 @@ We shall apply all the previous machinery to the study of regular languages
 and the constructions of the associated finite automata. *)
 
 include "tutorial/chapter7.ma".
+include "basics/core_notation/card_1.ma".
 
 (* The type re of regular expressions over an alphabet $S$ is the smallest 
 collection of objects generated by the following constructors: *)