I often use let expressions in Isar proofs to make things more readable, but Isabelle automatically unfolds these in the output, which makes reading it very cumbersome sometimes. Is it possible to disable this?

Use define instead

Syntax:

```
define x y where "x = foo" and "y = bar"
```

You get definition theorems `x_def`

and `y_def`

from this, similar to the `definition`

command.

For functions, you have to explicitly use lambda expressions (unlike with the `definition`

command):

```
define f where "f = (λx. …)"
```

I am still unsure if I prefer the λ or the `for`

version (the latter feels more regular in the Isar syntax):

```
define f where ‹f x = (x ∧ True)› for x
thm f_def (*f ?x = (?x ∧ True)*)
have ‹¬f False›
unfolding f_def by fast
```

I keep forgetting this even exists.

Manuel Eberl said:

I keep forgetting this even exists.

Me too...

Ujkan Sulejmani has marked this topic as resolved.

Last updated: Feb 27 2024 at 08:17 UTC