# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1622209386 -3600
# Node ID 370ce138d1bd51c65c919c30a2d47e0e4972ef1f
# Parent  493b1ae188dadd3c43a5b6d66c1c99f6cccf10f9
nicer statement of Liouville_theorem

diff -r 493b1ae188da -r 370ce138d1bd src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Wed May 26 18:07:49 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri May 28 14:43:06 2021 +0100
@@ -2482,12 +2482,13 @@
 theorem Liouville_theorem:
     assumes holf: "f holomorphic_on UNIV"
         and bf: "bounded (range f)"
-    obtains c where "\<And>z. f z = c"
+      shows "f constant_on UNIV"
 proof -
   obtain B where "\<And>z. cmod (f z) \<le> B"
     by (meson bf bounded_pos rangeI)
   then show ?thesis
-    using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
+    using Liouville_polynomial [OF holf, of 0 B 0, simplified]
+    by (meson constant_on_def)
 qed
 
 text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>