X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flibrary_auto%2Fauto%2Fnat%2Fprimes.ma;h=d4fb9e76ff6b2f760151316e879846ff0bee866d;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=21d752f71b6fcfe827dbc871723b20b55d4bae09;hpb=bbb9215a02e1321d01a11c0ead6d0d218d047f68;p=helm.git

diff --git a/helm/software/matita/contribs/library_auto/auto/nat/primes.ma b/helm/software/matita/contribs/library_auto/auto/nat/primes.ma
index 21d752f71..d4fb9e76f 100644
--- a/helm/software/matita/contribs/library_auto/auto/nat/primes.ma
+++ b/helm/software/matita/contribs/library_auto/auto/nat/primes.ma
@@ -22,9 +22,8 @@ include "auto/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/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m).
-interpretation "not divides" 'ndivides n m =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m)).
+interpretation "divides" 'divides n m = (divides n m).
+interpretation "not divides" 'ndivides n m = (Not (divides n m)).
 
 theorem reflexive_divides : reflexive nat divides.
 unfold reflexive.