X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2FQaxioms.ma;h=d527d657819656f3544b43decbc46343a1f5ecbd;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=da8e9e7a6813904e229ca631b91490c35932e1af;hpb=af130d273b6be7fbcc2fb2504f3b28ef8fa2344f;p=helm.git

diff --git a/helm/software/matita/library/Q/Qaxioms.ma b/helm/software/matita/library/Q/Qaxioms.ma
index da8e9e7a6..d527d6578 100644
--- a/helm/software/matita/library/Q/Qaxioms.ma
+++ b/helm/software/matita/library/Q/Qaxioms.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Q/Qaxioms".
-
 include "Z/compare.ma".
 include "Z/times.ma".
 include "nat/iteration2.ma".
@@ -68,4 +66,4 @@ definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus.
 (*
 theorem geometric: \forall q.\exists k. 
 Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)).
-*)  
\ No newline at end of file
+*)