diff --git a/Coq/Flocq/Core/Raux.theory.xml b/Coq/Flocq/Core/Raux.theory.xml index d0464f6..5949443 100644 --- a/Coq/Flocq/Core/Raux.theory.xml +++ b/Coq/Flocq/Core/Raux.theory.xml @@ -290,7 +290,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Core/Raux/radix_pos.con" as="Theorem" line="1333"/> - Well-used function called bpow for computing the power function β^e <ht:DEFINITION uri="cic:/Flocq/Core/Raux/bpow.con" as="Definition" line="1336"/> + Well-used function called bpow for computing the power function beta^e <ht:DEFINITION uri="cic:/Flocq/Core/Raux/bpow.con" as="Definition" line="1336"/> <ht:THEOREM uri="cic:/Flocq/Core/Raux/IZR_Zpower_pos.con" as="Theorem" line="1357"/> @@ -328,7 +328,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Core/Raux/sqrt_bpow_ge.con" as="Lemma" line="1571"/> - Another well-used function for having the magnitude of a real number x to the base β <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_prop.ind" as="Inductive" line="1574"/> + Another well-used function for having the magnitude of a real number x to the base beta <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_prop.ind" as="Inductive" line="1574"/> <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_val.con" as="Projection" line="1574"/> diff --git a/Coq/Flocq/Pff/Pff.theory.xml b/Coq/Flocq/Pff/Pff.theory.xml index 19bdd6b..16bcab8 100644 --- a/Coq/Flocq/Pff/Pff.theory.xml +++ b/Coq/Flocq/Pff/Pff.theory.xml @@ -3148,22 +3148,22 @@ It is the work of Sylvie Boldo, Marc Daumas, Laurence Rideau, and Laurent Théry </ht:SECTION> <a name="lab32"></a><h1 class="section">was file discriminant2.v</h1> This proof file has been written by -<A href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</A>(1), following a proof -presented by <A HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</A> (2), +<a href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</a>(1), following a proof +presented by <a HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</a> (2), and adapted to Coq proof checker with the help of -<A href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</A>(1) -and <A href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</A>(1). This work -has been partially supported by the <A HREF="http://www.cnrs.fr">CNRS</A> grant PICS 2533. +<a href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</a>(1) +and <a href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</a>(1). This work +has been partially supported by the <a HREF="http://www.cnrs.fr">CNRS</a> grant PICS 2533. <div class="paragraph"> </div> -(1) <A HREF="http://www.ens-lyon.fr/LIP/">LIP</A> Computer science laboratory +(1) <a HREF="http://www.ens-lyon.fr/LIP/">LIP</a> Computer science laboratory UMR 5668 CNRS - ENS de Lyon - INRIA Lyon, France <div class="paragraph"> </div> -(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</A> +(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</a> Berkeley, California <ht:SECTION uri="cic:/Flocq/Pff/Pff/Discriminant1" line="19370"> <ht:VARIABLE uri="cic:/Flocq/Pff/Pff/Discriminant1/bo.var" as="Assumption" line="19371"/> @@ -4308,22 +4308,22 @@ Berkeley, California </ht:SECTION> <a name="lab34"></a><h1 class="section">was file discriminant.v</h1> This proof file has been written by -<A href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</A>(1), following a proof -presented by <A HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</A> (2), +<a href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</a>(1), following a proof +presented by <a HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</a> (2), and adapted to Coq proof checker with the help of -<A href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</A>(1) -and <A href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</A>(1). This work -has been partially supported by the <A HREF="http://www.cnrs.fr">CNRS</A> grant PICS 2533. +<a href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</a>(1) +and <a href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</a>(1). This work +has been partially supported by the <a HREF="http://www.cnrs.fr">CNRS</a> grant PICS 2533. <div class="paragraph"> </div> -(1) <A HREF="http://www.ens-lyon.fr/LIP/">LIP</A> Computer science laboratory +(1) <a HREF="http://www.ens-lyon.fr/LIP/">LIP</a> Computer science laboratory UMR 5668 CNRS - ENS de Lyon - INRIA Lyon, France <div class="paragraph"> </div> -(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</A> +(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</a> Berkeley, California <ht:SECTION uri="cic:/Flocq/Pff/Pff/Discriminant5B" line="23211"> <ht:VARIABLE uri="cic:/Flocq/Pff/Pff/Discriminant5B/bo.var" as="Assumption" line="23212"/> diff --git a/Coq/Flocq/Prop/Relative.theory.xml b/Coq/Flocq/Prop/Relative.theory.xml index 521b72b..94bf766 100644 --- a/Coq/Flocq/Prop/Relative.theory.xml +++ b/Coq/Flocq/Prop/Relative.theory.xml @@ -83,7 +83,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error.con" as="Theorem" line="154"/> - 1+ε property in any rounding <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_ex.con" as="Theorem" line="168"/> + 1+epsilon property in any rounding <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_ex.con" as="Theorem" line="168"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_F2R_emin.con" as="Theorem" line="183"/> @@ -97,7 +97,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N.con" as="Theorem" line="290"/> - 1+ε property in rounding to nearest <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_ex.con" as="Theorem" line="307"/> + 1+epsilon property in rounding to nearest <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_ex.con" as="Theorem" line="307"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_F2R_emin.con" as="Theorem" line="329"/> @@ -121,7 +121,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX.con" as="Theorem" line="446"/> - 1+ε property in any rounding in FLX <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_ex.con" as="Theorem" line="458"/> + 1+epsilon property in any rounding in FLX <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_ex.con" as="Theorem" line="458"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_round.con" as="Theorem" line="472"/> @@ -141,7 +141,7 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX'.con" as="Theorem" line="573"/> - 1+ε property in rounding to nearest in FLX <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX_ex.con" as="Theorem" line="589"/> + 1+epsilon property in rounding to nearest in FLX <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX_ex.con" as="Theorem" line="589"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX'_ex.con" as="Theorem" line="601"/> @@ -171,13 +171,13 @@ COPYING file for more details. <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_F2R_emin_ex.con" as="Theorem" line="710"/> - 1+ε property in any rounding in FLT <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_ex.con" as="Theorem" line="723"/> + 1+epsilon property in any rounding in FLT <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_ex.con" as="Theorem" line="723"/> <ht:VARIABLE uri="cic:/Flocq/Prop/Relative/Fprop_relative/Fprop_relative_FLT/choice.var" as="Assumption" line="725"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT.con" as="Theorem" line="735"/> - 1+ε property in rounding to nearest in FLT <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_ex.con" as="Theorem" line="752"/> + 1+epsilon property in rounding to nearest in FLT <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_ex.con" as="Theorem" line="752"/> <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_round.con" as="Theorem" line="762"/>