--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Sep 24 14:30:09 2018 +0200
@@ -262,7 +262,7 @@
lift_definition one_ennreal :: ennreal is 1 by simp
lift_definition zero_ennreal :: ennreal is 0 by simp
lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(+)" by simp
-lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "( * )" by simp
+lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(*)" by simp
instance
by standard (transfer; auto simp: field_simps ereal_right_distrib)+