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