changed base uri

diff --git a/helm/software/matita/library_auto/Q/q.ma b/helm/software/matita/library_auto/Q/q.ma
index cf60105b9d1bc02ebbea2c537b09cf64d6bb23a0..d78400ea05e4df5fa725acb04daf4b87db03ecd6 100644 (file)
--- 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 8a1a6e1f046846410ab13c03c10985865f942905..c57e16672e4d660d47a0dd1afe6b4e0384245bd4 100644 (file)
--- 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 d3eafe4bd9762cccb9e6a0e0093fd63fda06c89c..4e912bb655733a74bb7bb792979b701d10d6af21 100644 (file)
--- 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 945d52cc63f670b0f13c93db085245121e21fd09..3cadd81d3cec3d8514641bf1d15753245b1b2b2b 100644 (file)
--- 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 53bcba9939aa09323eabcfa48fb237a33653992e..e80828ae98769dfa36a2872f5f83476dc40eb55d 100644 (file)
--- 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 85728d4c980e5dad57a4187032d99e9955f38d32..c628064b306c887447d2afd3ed97abca133c5ed2 100644 (file)
--- 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 0ce46753ff628d7c5eac126c8509cb3711679b9d..ae02688a055a2bde1c86d4080a174fa7de9a6965 100644 (file)
--- 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 89107fdee0efb006f003f552e6a25a3d7a7dfa4a..4c432296e81230968143f6b78cbaa3980e6cb8b7 100644 (file)
--- 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 72402f83ed3a97e716f5de3e5c6c0bbcccd972a6..73daf90f6e11d616b415c14d7b3f8473d0160b9e 100644 (file)
--- 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 0eb6139f678eff3ca4603ce7ce14cf35d325ba33..8a96d23f145a7fb95f3d435f6dff1214b6e283f0 100644 (file)
--- 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 ad83dbbaa85cc2fd2d0154934ea90dc9f76e5b3f..a2e83d1a0d879231bf255887e4916faf45d5f774 100644 (file)
--- 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 2a8449324867034d18acd01ffcb23cbe17a87ae1..0ccc4d0af63b60682caf95d44b133b320bb86f82 100644 (file)
--- 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 55352d04670a90e33a352689c18093b545288044..12c132186af1d2fd481b3c75a9838b1e37bf81b9 100644 (file)
--- 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 2c77ca5b5f7f41d07ee97597837f6a50788900b4..dedf1767f5ba9b6c7302f80faced8e5760a71a5c 100644 (file)
--- 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 6ee698849fcb18f7bae5ae730f70ad40084e4b4f..590683e7b55b10afcd2bf34971e134078389176c 100644 (file)
--- 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 579fbc76806c849cee2a516585543f5eecf8fe7d..9adb75a41c01326ec3e4f612ff9b2152cc6e0a44 100644 (file)
--- 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 7bab1da63f58d0c4eb37e8b2135bd4de3f483cd3..297196ccb8d615fe73ba8fec8281d7f1ea1f312f 100644 (file)
--- 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 6167e2dfb16e6e7b68446909efa16819ec04fa2d..55a9c7e82077fc1484099050129644e0a24ac4b4 100644 (file)
--- 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 3bb8cbc6e826ec2b36b25154bd5b4e0b5a6673ce..dabfcf8356c73cc8edc1284eb2c340a4e7aa66c3 100644 (file)
--- 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 dcab4d69f13ffec21e064044fd828eb87955dd70..d686d9f8945d591f373610b7a309a9d3ae18d824 100644 (file)
--- 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 d5f91db6ffa36e942d8f0dd8d0429b9ba5dcf0fd..c940e4e6c3360235f92fa7dc5d5569d4ab8689b8 100644 (file)
--- 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 c2d070a8fad66b06d1b1f6975fe2f36a9f027e87..3fbf92a292a0b4ae30c0e7eaa90a35aaffe0974f 100644 (file)
--- 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 80f5939dd0a25be7a245f8eeeaabac8138f1690c..b8eacad4ea6794ad338304775e8e7c1b1f8f651c 100644 (file)
--- 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 eabb598f1a95022a4b740b4c62375c894600bd8b..91e66f741184983e71681428f6f8ced1e180013c 100644 (file)
--- 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 8f73f0478170e50a582f9b853b5ac9328d32d83b..3527ac45a5b507e4abcd4a9396be7bdaff78e097 100644 (file)
--- 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 fb6b597e236aaccac9c15ba5079489d3149d0964..5dcfa647144fe234c8ba1cd83d24040d41c18569 100644 (file)
--- 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 e450fc3290be5a8e1b7dc9f4cac8a14301abf252..b560d940819e2fcfa304160caf3e050063be930b 100644 (file)
--- 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 b1bd03c86d2675a9cc6d6d8822bce6510ec4600a..4855b23cea3d8c68f355b19783728d412b20d02e 100644 (file)
--- 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 978b259c21a093083bc08a86dfc9cca66a409d48..af6d9245bebd393160d9d91cebf84dceca3ea977 100644 (file)
--- 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 59881be7b01efc7df17095179b3d60016cf98b02..f905d2120236487afcd8f87ae01e61f97ae75134 100644 (file)
--- 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 a8824eb90fc4b5c0ca02fb4f53aa98a1be943e7d..983e7644fd7c44d9f743f076da84ffe01f573298 100644 (file)
--- 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 cd2005309485f50abb5f2701c35c48df4e6ea9dc..60ebc0347cdb1ee3540b509dae7180844104bb2f 100644 (file)
--- 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 6826948196b9e75e36647f1f2702eef7ae493681..f95399a302ffe7ce137d336f7bd52e48c0dfee7c 100644 (file)
--- 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".