helm/papers/calculemus-2003/slides/misc/hint2.xml

   1 <?xml version="1.0"?>
   2 <hint id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0">
   3   <hints>
   4     <apply>cic:/Coq/Reals/Cv_prop/UL_suite.con</apply>
   5     <apply>cic:/Coq/Reals/R_sqr/Rsqr_inj.con</apply>
   6     <apply>cic:/Coq/Reals/R_sqrt/sqrt_inj.con</apply>
   7     <apply>cic:/Coq/Reals/Ranalysis1/unicite_limite.con</apply>
   8     <apply>cic:/Coq/Reals/Ranalysis1/unicite_step1.con</apply>
   9     <apply>cic:/Coq/Reals/Rbase/Rge_ge_eq.con</apply>
  10     <apply>cic:/Coq/Reals/Rbase/Rle_antisym.con</apply>
  11     <apply>cic:/Coq/Reals/Rbase/Rminus_eq.con</apply>
  12     <apply>cic:/Coq/Reals/Rbase/Rminus_eq_right.con</apply>
  13     <apply>cic:/Coq/Reals/Rbase/r_Rmult_mult.con</apply>
  14     <apply>cic:/Coq/Reals/Rbase/r_Rplus_plus.con</apply>
  15     <apply>cic:/Coq/Reals/Rcomplet/cond_eq.con</apply>
  16     <apply>cic:/Coq/Reals/Rlimit/single_limit.con</apply>
  17     <apply>cic:/Coq/Reals/Rlimit/tech_limit.con</apply>
  18     <apply>cic:/Coq/Reals/Rpower/exp_inv.con</apply>
  19     <apply>cic:/Coq/Reals/Rpower/ln_inv.con</apply>
  20     <apply>cic:/Coq/Reals/Rsqrt_def/cv_dicho.con</apply>
  21     <apply>cic:/Coq/Reals/Rtopology/is_lub_u.con</apply>
  22     <apply>cic:/Coq/Reals/Rtrigo_calc/toRad_inj.con</apply>
  23     <apply>cic:/Coq/Reals/Rtrigo_def/unicite_sum.con</apply>
  24     <apply>cic:/Rocq/AILS/ycngstys/eq_sym.con</apply>
  25   </hints>
  26 </hint>