`HOL-Example.Rewrite_Examples`

contains applications of both `rewrite at`

and `rewrite in`

. Unfortunately, from the examples I cannot tell what the difference between the two is. Could anyone tell me?

For `rewrite at`

you give the exact position where the rewriting should happen and for `rewrite in`

any subterm of the position works

This is what I had expected, but it is not what I experience: It seems that also with `at`

subterms are considered as well. For example, in the following code snippet rewriting is successful and the proof is accepted:

```
lemma "1 = Suc 0"
by (rewrite at "⌑" One_nat_def) (fact refl)
```

Last updated: Dec 07 2023 at 08:19 UTC