Skip to content
Snippets Groups Projects
Normal view Permalink
flocq 8.16 KiB
Newer Older
Jakob Albert's avatar
Add patch-framework and patches
Jakob Albert committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 
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 &beta;^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 &beta;  <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+&epsilon; 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+&epsilon; 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+&epsilon; 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+&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"/>
+ 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+&epsilon; 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+&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"/>
+ 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"/>