update in standard library

+ some notations with ^ decentralized
+ one decentralized notation added to reverse_complexity/speedup.ma

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 654185c89cb014f498e0bff30a9a0b63b8a4333a..5c7500dd976f5f4e9afcc5e0760c5ba156e9fcb5 100644 (file)
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/div_and_mod.ma".
+include "basics/core_notation/exp_2.ma".
 
 let rec exp n m on m ≝ 
  match m with 
@@ -182,4 +183,4 @@ qed.
 
   
    
-   
\ No newline at end of file
+   

diff --git a/matita/matita/lib/arithmetics/iteration.ma b/matita/matita/lib/arithmetics/iteration.ma
index 78d4eb4d01f67a852cd1544ced197c5bb91d7105..407e12b032429c0a430d8104f37768688fca446f 100644 (file)
--- a/matita/matita/lib/arithmetics/iteration.ma
+++ b/matita/matita/lib/arithmetics/iteration.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/nat.ma".
+include "basics/core_notation/exp_2.ma".
 
 (* iteration *) 
 
@@ -43,4 +44,4 @@ lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j →
   g^i a ≤  g^j a.
 #g #a #i #j #leg #leij elim leij //
 #m #leim #Hind normalize @(transitive_le … Hind) @leg 
-qed.
\ No newline at end of file
+qed.

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index 4d1e355a304d695725cbfe62530607f886fcd2b7..4ed9f326c1f239464b335f56964d6027809df4b2 100644 (file)
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -280,13 +280,6 @@ for @{ 'union $a $b }. (* \cup *)
 
 (* other notations **********************************************************)
 
-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}.
-notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
-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}.

diff --git a/matita/matita/lib/basics/core_notation/exp_2.ma b/matita/matita/lib/basics/core_notation/exp_2.ma
new file mode 100644 (file)
index 0000000..c5cd9dd
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/exp_2.ma
@@ -0,0 +1,16 @@
+(*
+    ||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 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/invert_1.ma b/matita/matita/lib/basics/core_notation/invert_1.ma
new file mode 100644 (file)
index 0000000..14f5692
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/invert_1.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 "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.

diff --git a/matita/matita/lib/basics/core_notation/invert_appl_2.ma b/matita/matita/lib/basics/core_notation/invert_appl_2.ma
new file mode 100644 (file)
index 0000000..57a9eeb
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/invert_appl_2.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 < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. 

diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma
index 02605e4a87da4ab6491c1ff9467311d76db311b5..94a8d22ebb6f69dd64c249677e30c74ee7fdb9d3 100644 (file)
--- a/matita/matita/lib/formal_topology/categories.ma
+++ b/matita/matita/lib/formal_topology/categories.ma
@@ -14,6 +14,7 @@
 
 include "formal_topology/cprop_connectives.ma".
 include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/invert_1.ma".
 
 inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝
     refl: eq A x x.

diff --git a/matita/matita/lib/reverse_complexity/speedup.ma b/matita/matita/lib/reverse_complexity/speedup.ma
index f1e56d5600f9d11cfae0898ce2d14918febc1466..52b7db0ddc9e9ab800eae0a09bf40bd8ab3dbfc7 100644 (file)
--- a/matita/matita/lib/reverse_complexity/speedup.ma
+++ b/matita/matita/lib/reverse_complexity/speedup.ma
@@ -1,4 +1,5 @@
 include "reverse_complexity/bigops_compl.ma".
+include "basics/core_notation/napart_2.ma".
 
 (********************************* the speedup ********************************)
 
@@ -569,4 +570,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/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index 72e396c133ea84026a0898fae69eb4069d488eef..07a5fd19f04586d76a2bfa627ede33b789a69c9d 100644 (file)
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -16,6 +16,7 @@ include "basics/relations.ma".
 include "basics/types.ma".
 include "arithmetics/nat.ma".
 include "hints_declaration.ma".
+include "basics/core_notation/invert_1.ma".
 
 (******************* Quotienting in type theory **********************)