--- a/CONTRIBUTORS Thu Jan 18 17:04:35 2018 +0100
+++ b/CONTRIBUTORS Fri Jan 19 08:28:08 2018 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* January 2018: Sebastien Gouezel
+ Various small additions to HOL-Analysis
+
* December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
A new conditional parametricity prover.
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jan 18 17:04:35 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 19 08:28:08 2018 +0100
@@ -923,6 +923,9 @@
lemma e2ennreal_enn2ereal[simp]: "e2ennreal (enn2ereal x) = x"
by (simp add: e2ennreal_def max_absorb2 ennreal.enn2ereal_inverse)
+lemma enn2ereal_e2ennreal: "x \<ge> 0 \<Longrightarrow> enn2ereal (e2ennreal x) = x"
+by (metis e2ennreal_enn2ereal ereal_ennreal_cases not_le)
+
lemma e2ennreal_ereal [simp]: "e2ennreal (ereal x) = ennreal x"
by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)