when I ctrl + click on Abs_filter :: "(('a ⇒ bool) ⇒ bool) ⇒ 'a filter" I get:

```
locale is_filter =
fixes F :: "('a ⇒ bool) ⇒ bool"
assumes True: "F (λx. True)"
assumes conj: "F (λx. P x) ⟹ F (λx. Q x) ⟹ F (λx. P x ∧ Q x)"
assumes mono: "∀x. P x ⟶ Q x ⟹ F (λx. P x) ⟹ F (λx. Q x)"
typedef 'a filter = "{F :: ('a ⇒ bool) ⇒ bool. is_filter F}"
proof
show "(λx. True) ∈ ?filter" by (auto intro: is_filter.intro)
qed
```

I am confused about how to map F::"('a ⇒ bool) ⇒ bool" into 'a filter?

Query panel > find constants > `‹(_ ⇒ bool) ⇒ _ filter›`

but I am confused by your question: what don't you understand?

that `Abs_filter F`

is a filter?

Can someone explain the difference between `notation`

and `syntax`

?

`notation`

only allows relatively simple infix/mixfix syntax for constants; `syntax`

allows introducing more complex syntactic features. For more details, look at Chapter 8 of the Isabelle/Isar reference manual.

thanks Manuel

I wouldn't worry too much about it though; I've been using Isabelle for 10 years and I still don't really understand `syntax`

and `translation`

. If there's anything concrete that you want to achieve and you can't figure it out by looking e.g. at other stuff in the library, maybe ask the concrete question here.

As a regular Isabelle user, I think it's not too fruitful to invest time and effort into learning how these work

Last updated: Aug 13 2022 at 06:26 UTC