From: Cristian Armentano <??>
Date: Fri, 20 Apr 2007 10:06:10 +0000 (+0000)
Subject: changed base uri
X-Git-Tag: make_still_working~6373
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=af1498c45e1266fc08923eeaeb5c3cb7fc7776e6;p=helm.git

changed base uri
---

diff --git a/helm/software/matita/library_auto/Q/q.ma b/helm/software/matita/library_auto/Q/q.ma
index cf60105b9..d78400ea0 100644
--- a/helm/software/matita/library_auto/Q/q.ma
+++ b/helm/software/matita/library_auto/Q/q.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Q/q".
+set "baseuri" "cic:/matita/library_auto/Q/q".
 
 include "Z/compare.ma".
 include "Z/plus.ma".
diff --git a/helm/software/matita/library_auto/Z/compare.ma b/helm/software/matita/library_auto/Z/compare.ma
index 8a1a6e1f0..c57e16672 100644
--- a/helm/software/matita/library_auto/Z/compare.ma
+++ b/helm/software/matita/library_auto/Z/compare.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/compare".
+set "baseuri" "cic:/matita/library_auto/Z/compare".
 
 include "Z/orders.ma".
 include "nat/compare.ma".
diff --git a/helm/software/matita/library_auto/Z/orders.ma b/helm/software/matita/library_auto/Z/orders.ma
index d3eafe4bd..4e912bb65 100644
--- a/helm/software/matita/library_auto/Z/orders.ma
+++ b/helm/software/matita/library_auto/Z/orders.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/orders".
+set "baseuri" "cic:/matita/library_auto/Z/orders".
 
 include "Z/z.ma".
 include "nat/orders.ma".
@@ -37,10 +37,10 @@ definition Zle : Z \to Z \to Prop \def
     | (neg m) \Rightarrow m \leq n ]].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
+interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/library_auto/Z/orders/Zle.con x y).
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'neither less nor equal to'" 'nleq x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/Z/orders/Zle.con x y)).
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -62,10 +62,10 @@ definition Zlt : Z \to Z \to Prop \def
     | (neg m) \Rightarrow m<n ]].
     
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
+interpretation "integer 'less than'" 'lt x y = (cic:/matita/library_auto/Z/orders/Zlt.con x y).
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'not less than'" 'nless x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/Z/orders/Zlt.con x y)).
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
 unfold irreflexive.
diff --git a/helm/software/matita/library_auto/Z/plus.ma b/helm/software/matita/library_auto/Z/plus.ma
index 945d52cc6..3cadd81d3 100644
--- a/helm/software/matita/library_auto/Z/plus.ma
+++ b/helm/software/matita/library_auto/Z/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/plus".
+set "baseuri" "cic:/matita/library_auto/Z/plus".
 
 include "Z/z.ma".
 include "nat/minus.ma".
@@ -41,7 +41,7 @@ definition Zplus :Z \to Z \to Z \def
          | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).
+interpretation "integer plus" 'plus x y = (cic:/matita/library_auto/Z/plus/Zplus.con x y).
          
 theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
 intro.
@@ -409,7 +409,7 @@ definition Zopp : Z \to Z \def
 | (neg n) \Rightarrow (pos n) ].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x).
+interpretation "integer unary minus" 'uminus x = (cic:/matita/library_auto/Z/plus/Zopp.con x).
 
 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
 intros.
@@ -467,4 +467,4 @@ qed.
 (* minus *)
 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
 
-interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y).
+interpretation "integer minus" 'minus x y = (cic:/matita/library_auto/Z/plus/Zminus.con x y).
diff --git a/helm/software/matita/library_auto/Z/times.ma b/helm/software/matita/library_auto/Z/times.ma
index 53bcba993..e80828ae9 100644
--- a/helm/software/matita/library_auto/Z/times.ma
+++ b/helm/software/matita/library_auto/Z/times.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/times".
+set "baseuri" "cic:/matita/library_auto/Z/times".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".
@@ -33,7 +33,7 @@ definition Ztimes :Z \to Z \to Z \def
          | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
          
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
+interpretation "integer times" 'times x y = (cic:/matita/library_auto/Z/times/Ztimes.con x y).
 
 theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
 intro.
diff --git a/helm/software/matita/library_auto/Z/z.ma b/helm/software/matita/library_auto/Z/z.ma
index 85728d4c9..c628064b3 100644
--- a/helm/software/matita/library_auto/Z/z.ma
+++ b/helm/software/matita/library_auto/Z/z.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Z/z".
+set "baseuri" "cic:/matita/library_auto/Z/z".
 
 include "datatypes/bool.ma".
 include "nat/nat.ma".
@@ -27,7 +27,7 @@ definition Z_of_nat \def
 [ O \Rightarrow  OZ 
 | (S n)\Rightarrow  pos n].
 
-coercion cic:/matita/Z/z/Z_of_nat.con.
+coercion cic:/matita/library_auto/Z/z/Z_of_nat.con.
 
 definition neg_Z_of_nat \def
 \lambda n. match n with
diff --git a/helm/software/matita/library_auto/nat/chinese_reminder.ma b/helm/software/matita/library_auto/nat/chinese_reminder.ma
index 0ce46753f..ae02688a0 100644
--- a/helm/software/matita/library_auto/nat/chinese_reminder.ma
+++ b/helm/software/matita/library_auto/nat/chinese_reminder.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chinese_reminder".
+set "baseuri" "cic:/matita/library_auto/nat/chinese_reminder".
 
 include "nat/exp.ma".
 include "nat/gcd.ma".
diff --git a/helm/software/matita/library_auto/nat/compare.ma b/helm/software/matita/library_auto/nat/compare.ma
index 89107fdee..4c432296e 100644
--- a/helm/software/matita/library_auto/nat/compare.ma
+++ b/helm/software/matita/library_auto/nat/compare.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/compare".
+set "baseuri" "cic:/matita/library_auto/nat/compare".
 
 include "datatypes/bool.ma".
 include "datatypes/compare.ma".
diff --git a/helm/software/matita/library_auto/nat/congruence.ma b/helm/software/matita/library_auto/nat/congruence.ma
index 72402f83e..73daf90f6 100644
--- a/helm/software/matita/library_auto/nat/congruence.ma
+++ b/helm/software/matita/library_auto/nat/congruence.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/congruence".
+set "baseuri" "cic:/matita/library_auto/nat/congruence".
 
 include "nat/relevant_equations.ma".
 include "nat/primes.ma".
@@ -24,7 +24,7 @@ definition congruent: nat \to nat \to nat \to Prop \def
 \lambda n,m,p:nat. mod n p = mod m p.
 
 interpretation "congruent" 'congruent n m p =
-  (cic:/matita/nat/congruence/congruent.con n m p).
+  (cic:/matita/library_auto/nat/congruence/congruent.con n m p).
 
 notation < "hvbox(n break \cong\sub p m)"
   (*non associative*) with precedence 45
diff --git a/helm/software/matita/library_auto/nat/count.ma b/helm/software/matita/library_auto/nat/count.ma
index 0eb6139f6..8a96d23f1 100644
--- a/helm/software/matita/library_auto/nat/count.ma
+++ b/helm/software/matita/library_auto/nat/count.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/count".
+set "baseuri" "cic:/matita/library_auto/nat/count".
 
 include "nat/relevant_equations.ma".
 include "nat/sigma_and_pi.ma".
diff --git a/helm/software/matita/library_auto/nat/div_and_mod.ma b/helm/software/matita/library_auto/nat/div_and_mod.ma
index ad83dbbaa..a2e83d1a0 100644
--- a/helm/software/matita/library_auto/nat/div_and_mod.ma
+++ b/helm/software/matita/library_auto/nat/div_and_mod.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/div_and_mod".
+set "baseuri" "cic:/matita/library_auto/nat/div_and_mod".
 
 include "datatypes/constructors.ma".
 include "nat/minus.ma".
@@ -32,7 +32,7 @@ match m with
 | (S p) \Rightarrow mod_aux n n p]. 
 
 interpretation "natural remainder" 'module x y =
-  (cic:/matita/nat/div_and_mod/mod.con x y).
+  (cic:/matita/library_auto/nat/div_and_mod/mod.con x y).
 
 let rec div_aux p m n : nat \def
 match (leb m n) with
@@ -49,7 +49,7 @@ match m with
 | (S p) \Rightarrow div_aux n n p]. 
 
 interpretation "natural divide" 'divide x y =
-  (cic:/matita/nat/div_and_mod/div.con x y).
+  (cic:/matita/library_auto/nat/div_and_mod/div.con x y).
 
 theorem le_mod_aux_m_m: 
 \forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
diff --git a/helm/software/matita/library_auto/nat/euler_theorem.ma b/helm/software/matita/library_auto/nat/euler_theorem.ma
index 2a8449324..0ccc4d0af 100644
--- a/helm/software/matita/library_auto/nat/euler_theorem.ma
+++ b/helm/software/matita/library_auto/nat/euler_theorem.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/euler_theorem".
+set "baseuri" "cic:/matita/library_auto/nat/euler_theorem".
 
 include "nat/map_iter_p.ma".
 include "nat/totient.ma".
diff --git a/helm/software/matita/library_auto/nat/exp.ma b/helm/software/matita/library_auto/nat/exp.ma
index 55352d046..12c132186 100644
--- a/helm/software/matita/library_auto/nat/exp.ma
+++ b/helm/software/matita/library_auto/nat/exp.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/exp".
+set "baseuri" "cic:/matita/library_auto/nat/exp".
 
 include "nat/div_and_mod.ma".
 
@@ -21,7 +21,7 @@ let rec exp n m on m\def
  [ O \Rightarrow (S O)
  | (S p) \Rightarrow (times n (exp n p)) ].
 
-interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (cic:/matita/library_auto/nat/exp/exp.con a b).
 
 theorem exp_plus_times : \forall n,p,q:nat. 
 n \sup (p + q) = (n \sup p) * (n \sup q).
diff --git a/helm/software/matita/library_auto/nat/factorial.ma b/helm/software/matita/library_auto/nat/factorial.ma
index 2c77ca5b5..dedf1767f 100644
--- a/helm/software/matita/library_auto/nat/factorial.ma
+++ b/helm/software/matita/library_auto/nat/factorial.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorial".
+set "baseuri" "cic:/matita/library_auto/nat/factorial".
 
 include "nat/le_arith.ma".
 
@@ -21,7 +21,7 @@ let rec fact n \def
   [ O \Rightarrow (S O)
   | (S m) \Rightarrow (S m)*(fact m)].
 
-interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n).
+interpretation "factorial" 'fact n = (cic:/matita/library_auto/nat/factorial/fact.con n).
 
 theorem le_SO_fact : \forall n. (S O) \le n!.
 intro.
diff --git a/helm/software/matita/library_auto/nat/factorization.ma b/helm/software/matita/library_auto/nat/factorization.ma
index 6ee698849..590683e7b 100644
--- a/helm/software/matita/library_auto/nat/factorization.ma
+++ b/helm/software/matita/library_auto/nat/factorization.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorization".
+set "baseuri" "cic:/matita/library_auto/nat/factorization".
 
 include "nat/ord.ma".
 include "nat/gcd.ma".
diff --git a/helm/software/matita/library_auto/nat/fermat_little_theorem.ma b/helm/software/matita/library_auto/nat/fermat_little_theorem.ma
index 579fbc768..9adb75a41 100644
--- a/helm/software/matita/library_auto/nat/fermat_little_theorem.ma
+++ b/helm/software/matita/library_auto/nat/fermat_little_theorem.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/fermat_little_theorem".
+set "baseuri" "cic:/matita/library_auto/nat/fermat_little_theorem".
 
 include "nat/exp.ma".
 include "nat/gcd.ma".
diff --git a/helm/software/matita/library_auto/nat/gcd.ma b/helm/software/matita/library_auto/nat/gcd.ma
index 7bab1da63..297196ccb 100644
--- a/helm/software/matita/library_auto/nat/gcd.ma
+++ b/helm/software/matita/library_auto/nat/gcd.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd".
+set "baseuri" "cic:/matita/library_auto/nat/gcd".
 
 include "nat/primes.ma".
 
diff --git a/helm/software/matita/library_auto/nat/le_arith.ma b/helm/software/matita/library_auto/nat/le_arith.ma
index 6167e2dfb..55a9c7e82 100644
--- a/helm/software/matita/library_auto/nat/le_arith.ma
+++ b/helm/software/matita/library_auto/nat/le_arith.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/le_arith".
+set "baseuri" "cic:/matita/library_auto/nat/le_arith".
 
 include "nat/times.ma".
 include "nat/orders.ma".
diff --git a/helm/software/matita/library_auto/nat/lt_arith.ma b/helm/software/matita/library_auto/nat/lt_arith.ma
index 3bb8cbc6e..dabfcf835 100644
--- a/helm/software/matita/library_auto/nat/lt_arith.ma
+++ b/helm/software/matita/library_auto/nat/lt_arith.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/lt_arith".
+set "baseuri" "cic:/matita/library_auto/nat/lt_arith".
 
 include "nat/div_and_mod.ma".
 
diff --git a/helm/software/matita/library_auto/nat/map_iter_p.ma b/helm/software/matita/library_auto/nat/map_iter_p.ma
index dcab4d69f..d686d9f89 100644
--- a/helm/software/matita/library_auto/nat/map_iter_p.ma
+++ b/helm/software/matita/library_auto/nat/map_iter_p.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/map_iter_p.ma".
+set "baseuri" "cic:/matita/library_auto/nat/map_iter_p.ma".
 
 include "nat/permutation.ma".
 include "nat/count.ma".
diff --git a/helm/software/matita/library_auto/nat/minimization.ma b/helm/software/matita/library_auto/nat/minimization.ma
index d5f91db6f..c940e4e6c 100644
--- a/helm/software/matita/library_auto/nat/minimization.ma
+++ b/helm/software/matita/library_auto/nat/minimization.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/minimization".
+set "baseuri" "cic:/matita/library_auto/nat/minimization".
 
 include "nat/minus.ma".
 
diff --git a/helm/software/matita/library_auto/nat/minus.ma b/helm/software/matita/library_auto/nat/minus.ma
index c2d070a8f..3fbf92a29 100644
--- a/helm/software/matita/library_auto/nat/minus.ma
+++ b/helm/software/matita/library_auto/nat/minus.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
+set "baseuri" "cic:/matita/library_auto/nat/minus".
 
 include "nat/le_arith.ma".
 include "nat/compare.ma".
@@ -27,7 +27,7 @@ let rec minus n m \def
         | (S q) \Rightarrow minus p q ]].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (cic:/matita/library_auto/nat/minus/minus.con x y).
 
 theorem minus_n_O: \forall n:nat.n=n-O.
 intros.
diff --git a/helm/software/matita/library_auto/nat/nat.ma b/helm/software/matita/library_auto/nat/nat.ma
index 80f5939dd..b8eacad4e 100644
--- a/helm/software/matita/library_auto/nat/nat.ma
+++ b/helm/software/matita/library_auto/nat/nat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/nat".
+set "baseuri" "cic:/matita/library_auto/nat/nat".
 
 include "higher_order_defs/functions.ma".
 
diff --git a/helm/software/matita/library_auto/nat/nth_prime.ma b/helm/software/matita/library_auto/nat/nth_prime.ma
index eabb598f1..91e66f741 100644
--- a/helm/software/matita/library_auto/nat/nth_prime.ma
+++ b/helm/software/matita/library_auto/nat/nth_prime.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/nth_prime".
+set "baseuri" "cic:/matita/library_auto/nat/nth_prime".
 
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
diff --git a/helm/software/matita/library_auto/nat/ord.ma b/helm/software/matita/library_auto/nat/ord.ma
index 8f73f0478..3527ac45a 100644
--- a/helm/software/matita/library_auto/nat/ord.ma
+++ b/helm/software/matita/library_auto/nat/ord.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/ord".
+set "baseuri" "cic:/matita/library_auto/nat/ord".
 
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
diff --git a/helm/software/matita/library_auto/nat/orders.ma b/helm/software/matita/library_auto/nat/orders.ma
index fb6b597e2..5dcfa6471 100644
--- a/helm/software/matita/library_auto/nat/orders.ma
+++ b/helm/software/matita/library_auto/nat/orders.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders".
+set "baseuri" "cic:/matita/library_auto/nat/orders".
 
 include "nat/nat.ma".
 include "higher_order_defs/ordering.ma".
@@ -23,35 +23,35 @@ inductive le (n:nat) : nat \to Prop \def
   | le_S : \forall m:nat. le n m \to le n (S m).
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y).
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'neither less nor equal to'" 'nleq x y =
   (cic:/matita/logic/connectives/Not.con
-    (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
+    (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y)).
 
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
+interpretation "natural 'less than'" 'lt x y = (cic:/matita/library_auto/nat/orders/lt.con x y).
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'not less than'" 'nless x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/lt.con x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
+interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/library_auto/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+interpretation "natural 'greater than'" 'gt x y = (cic:/matita/library_auto/nat/orders/gt.con x y).
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'not greater than'" 'ngtr x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.
 unfold transitive.
diff --git a/helm/software/matita/library_auto/nat/permutation.ma b/helm/software/matita/library_auto/nat/permutation.ma
index e450fc329..b560d9408 100644
--- a/helm/software/matita/library_auto/nat/permutation.ma
+++ b/helm/software/matita/library_auto/nat/permutation.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/permutation".
+set "baseuri" "cic:/matita/library_auto/nat/permutation".
 
 include "nat/compare.ma".
 include "nat/sigma_and_pi.ma".
@@ -116,7 +116,7 @@ notation < "(❲i \atop j❳)n"
 for @{ 'transposition $i $j $n}.
 
 interpretation "natural transposition" 'transposition i j n =
-  (cic:/matita/nat/permutation/transpose.con i j n).
+  (cic:/matita/library_auto/nat/permutation/transpose.con i j n).
 
 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
 intros.
diff --git a/helm/software/matita/library_auto/nat/plus.ma b/helm/software/matita/library_auto/nat/plus.ma
index b1bd03c86..4855b23ce 100644
--- a/helm/software/matita/library_auto/nat/plus.ma
+++ b/helm/software/matita/library_auto/nat/plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/plus".
+set "baseuri" "cic:/matita/library_auto/nat/plus".
 
 include "nat/nat.ma".
 
@@ -22,7 +22,7 @@ let rec plus n m \def
  | (S p) \Rightarrow S (plus p m) ].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus" 'plus x y = (cic:/matita/nat/plus/plus.con x y).
+interpretation "natural plus" 'plus x y = (cic:/matita/library_auto/nat/plus/plus.con x y).
 
 theorem plus_n_O: \forall n:nat. n = n+O.
 intros.elim n
diff --git a/helm/software/matita/library_auto/nat/primes.ma b/helm/software/matita/library_auto/nat/primes.ma
index 978b259c2..af6d9245b 100644
--- a/helm/software/matita/library_auto/nat/primes.ma
+++ b/helm/software/matita/library_auto/nat/primes.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/primes".
+set "baseuri" "cic:/matita/library_auto/nat/primes".
 
 include "nat/div_and_mod.ma".
 include "nat/minimization.ma".
@@ -22,9 +22,9 @@ include "nat/factorial.ma".
 inductive divides (n,m:nat) : Prop \def
 witness : \forall p:nat.m = times n p \to divides n m.
 
-interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
+interpretation "divides" 'divides n m = (cic:/matita/library_auto/nat/primes/divides.ind#xpointer(1/1) n m).
 interpretation "not divides" 'ndivides n m =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/primes/divides.ind#xpointer(1/1) n m)).
 
 theorem reflexive_divides : reflexive nat divides.
 unfold reflexive.
diff --git a/helm/software/matita/library_auto/nat/relevant_equations.ma b/helm/software/matita/library_auto/nat/relevant_equations.ma
index 59881be7b..f905d2120 100644
--- a/helm/software/matita/library_auto/nat/relevant_equations.ma
+++ b/helm/software/matita/library_auto/nat/relevant_equations.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/relevant_equations".
+set "baseuri" "cic:/matita/library_auto/nat/relevant_equations".
 
 include "nat/times.ma".
 include "nat/minus.ma".
diff --git a/helm/software/matita/library_auto/nat/sigma_and_pi.ma b/helm/software/matita/library_auto/nat/sigma_and_pi.ma
index a8824eb90..983e7644f 100644
--- a/helm/software/matita/library_auto/nat/sigma_and_pi.ma
+++ b/helm/software/matita/library_auto/nat/sigma_and_pi.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/sigma_and_pi".
+set "baseuri" "cic:/matita/library_auto/nat/sigma_and_pi".
 
 include "nat/factorial.ma".
 include "nat/exp.ma".
diff --git a/helm/software/matita/library_auto/nat/times.ma b/helm/software/matita/library_auto/nat/times.ma
index cd2005309..60ebc0347 100644
--- a/helm/software/matita/library_auto/nat/times.ma
+++ b/helm/software/matita/library_auto/nat/times.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times".
+set "baseuri" "cic:/matita/library_auto/nat/times".
 
 include "nat/plus.ma".
 
@@ -22,7 +22,7 @@ let rec times n m \def
  | (S p) \Rightarrow m+(times p m) ].
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
+interpretation "natural times" 'times x y = (cic:/matita/library_auto/nat/times/times.con x y).
 
 theorem times_n_O: \forall n:nat. O = n*O.
 intros.elim n
diff --git a/helm/software/matita/library_auto/nat/totient.ma b/helm/software/matita/library_auto/nat/totient.ma
index 682694819..f95399a30 100644
--- a/helm/software/matita/library_auto/nat/totient.ma
+++ b/helm/software/matita/library_auto/nat/totient.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/totient".
+set "baseuri" "cic:/matita/library_auto/nat/totient".
 
 include "nat/count.ma".
 include "nat/chinese_reminder.ma".