I was wondering what is the symbol ‘ in the Isabelle tutorial main.pdf below (under the section "Set")?
(‘) :: ('a => 'b) => 'a set => 'b set
By looking into the symbols tab, the closest in shape I could find is \<acute> under the "Unsorted" category. I tried to evaluate the following expression, but it doesn't parse:
value "´ (λ(n::nat). n+1) {1,2}"
value "(λ(n::nat). n+1) ´ {1,2}"
Can anyone help to explain the usage here and what it does?
I believe that the symbol that you are looking for is `, not ‘ or ´. The symbol ` is an infix notation for the constant image that is defined in theory Set.thy in the main library of Isabelle/HOL. Hopefully, the name of the constant is self-explanatory. For completeness, I restate the definition in this answer:
definition image :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set" (infixr "`" 90)
where "f ` A = {y. ∃x∈A. y = f x}"
Thence,
value "(λ(n::nat). n+1) ` {1,2}"
evaluates to "{2, 3}" :: "nat set", as expected.