Is there a way to convert a theorem with schematic variables to a theorem with meta-quantified variables?

what difference do you make between both? If I try:

```
consts P :: \<open>nat \<Rightarrow> bool\<close>
lemma T1: \<open>P x\<close> for x
sorry
lemma T2: \<open>\<And>x. P x\<close>
sorry
lemma T3: \<open>P x\<close>
sorry
thm T1 T2 T3
(*
• P ?x
• P ?x
• P ?x
*)
```

The resulting theorems are all the same.

Like Mathias said, the two are mostly functionally the same from the end-user (non-ML) point of view. **EDIT**: Although maybe some things like the `where`

attribute won't work on quantified variables since those are bound..

If you are doing strange things, potentially the attribute `rule_format`

*might* help to normalise theorems to what you want (although it is not clear if this is a good idea or not).

Last updated: Aug 10 2022 at 19:17 UTC