X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fpapers%2Fcalculemus-2003%2Fslides%2Fmisc%2Fhint2.xml;fp=helm%2Fpapers%2Fcalculemus-2003%2Fslides%2Fmisc%2Fhint2.xml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=ab74769b7d8f5704de51f230b60f2c9cc019c1dc;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/papers/calculemus-2003/slides/misc/hint2.xml b/helm/papers/calculemus-2003/slides/misc/hint2.xml
deleted file mode 100644
index ab74769b7..000000000
--- a/helm/papers/calculemus-2003/slides/misc/hint2.xml
+++ /dev/null
@@ -1,26 +0,0 @@
-<?xml version="1.0"?>
-<hint id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0">
-  <hints>
-    <apply>cic:/Coq/Reals/Cv_prop/UL_suite.con</apply>
-    <apply>cic:/Coq/Reals/R_sqr/Rsqr_inj.con</apply>
-    <apply>cic:/Coq/Reals/R_sqrt/sqrt_inj.con</apply>
-    <apply>cic:/Coq/Reals/Ranalysis1/unicite_limite.con</apply>
-    <apply>cic:/Coq/Reals/Ranalysis1/unicite_step1.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/Rge_ge_eq.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/Rle_antisym.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/Rminus_eq.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/Rminus_eq_right.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/r_Rmult_mult.con</apply>
-    <apply>cic:/Coq/Reals/Rbase/r_Rplus_plus.con</apply>
-    <apply>cic:/Coq/Reals/Rcomplet/cond_eq.con</apply>
-    <apply>cic:/Coq/Reals/Rlimit/single_limit.con</apply>
-    <apply>cic:/Coq/Reals/Rlimit/tech_limit.con</apply>
-    <apply>cic:/Coq/Reals/Rpower/exp_inv.con</apply>
-    <apply>cic:/Coq/Reals/Rpower/ln_inv.con</apply>
-    <apply>cic:/Coq/Reals/Rsqrt_def/cv_dicho.con</apply>
-    <apply>cic:/Coq/Reals/Rtopology/is_lub_u.con</apply>
-    <apply>cic:/Coq/Reals/Rtrigo_calc/toRad_inj.con</apply>
-    <apply>cic:/Coq/Reals/Rtrigo_def/unicite_sum.con</apply>
-    <apply>cic:/Rocq/AILS/ycngstys/eq_sym.con</apply>
-  </hints>
-</hint>