diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Hull.thy --- 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 \A generic notion of the convex, affine, conic hull, or closed "hull".\ -definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) +definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl \hull\ 75) where "S hull s = \{t. S t \ s \ t}" lemma hull_same: "S s \ S hull s = s"