changed base uri

[helm.git] / helm / software / matita / library_auto / nat / primes.ma

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.