src/HOL/Hull.thy
changeset 80932 261cd8722677
parent 68189 6163c90694ef
--- a/src/HOL/Hull.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Hull.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -11,7 +11,7 @@
 
 subsection \<open>A generic notion of the convex, affine, conic hull, or closed "hull".\<close>
 
-definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
+definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl \<open>hull\<close> 75)
   where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
 
 lemma hull_same: "S s \<Longrightarrow> S hull s = s"