Suppose I have a theorem `OFCLASS(?'a::order, preorder_class) ⟹ (?y::?'a::order) ≤ (?z::?'a::order) ⟹ ?y ≤ ?z`

. Using Isabelle/ML, how can I obtain the theorem `(?y::?'a::order) ≤ (?z::?'a::order) ⟹ ?y ≤ ?z`

?

Ok, if the former theorem is bound to `thm`

then I can do:

```
thm OF [@{lemma ‹OFCLASS('a::order, preorder_class)› by intro_classes}]
```

But what If I don't know how x and y in `OFCLASS(x, y)`

look like?

The solution I found is the following:

```
val thm = ...
val assm = Goal.prove @{context} [] [] (hd (Thm.prems_of thm)) (K (Class.intro_classes_tac @{context} []))
val thm' = thm OF [assm]
```

Last updated: Aug 15 2022 at 04:16 UTC