changeset 75455 | 91c16c5ad3e9 |
parent 71698 | b69dc6bcbea3 |
child 78131 | 1cadc477f644 |
--- a/src/HOL/Analysis/Lipschitz.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Tue May 17 14:10:14 2022 +0100 @@ -623,7 +623,7 @@ by (simp add: dist_commute) subgoal using \<open>0 < u\<close> \<open>b \<in> X\<close> - by (simp add: ) + by simp done also have "(L + 1) * dist y b \<le> e / 2" using le1 \<open>0 \<le> L\<close> by simp