I found this expression somewhere in Isabelle's standard library and tried to see what value does with it
value "(λ x::bool . ¬x) ≤ (λ x . x)"
It outputs False. What is the meaning of ≤ here? Ideally, where can I find the exact instantiation of it? When I Ctrl+Click on the lambda symbol, jEdit doesn't take me anywhere. Is λ part of meta logic then? Where is it defined?
This and many other things are defined in Lattices.thy theory in Main library
https://isabelle.in.tum.de/library/HOL/HOL/Lattices.html
under the following section.
subsection ‹Lattice on \<^typ>‹_ ⇒ _››
instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin
definition "f ⊔ g = (λx. f x ⊔ g x)"
lemma sup_apply [simp, code]: "(f ⊔ g) x = f x ⊔ g x"
by (simp add: sup_fun_def)
instance
by standard (simp_all add: le_fun_def)
end