Paul Bachmann (Jun 16 2021 at 16:49): Paul Bachmann (Jun 16 2021 at 16:49):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.
Florian Sextl (Jun 16 2021 at 18:59):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: ).
Paul Bachmann (Jun 16 2021 at 19:49):Ahh, great, thank you! :)
Last updated: Nov 05 2025 at 08:30 UTC