I am looking for a way in ML to to turn the theorem `P (?x)`

into the theorem `⋀x. P (x)`

. Is there some function or a theorem that I use to do this? I already tried using `Thm.forall_intr`

but that's not quite it.

There is the function `forall_intr_vars`

that does exactly what you want. The correct usage is e.g. described in the "Isabelle Cookbook" (which is also where I found it :smile: ).

Ahh, great, thank you! :)

Last updated: Dec 07 2023 at 16:21 UTC