[isabelle-dev] Backticks and schematic variables

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Sep 9 16:58:23 CEST 2010

Hi all,

I was wondering if there's a reason why facts with backticks can't contain schematic variables. For example,

    thm `?s = ?t ⟹ ?t = ?s`


    *** Unbound schematic variable: ?s
    *** At command "thm"

That theorem in particular has a name ("sym"), but when local or chained facts have no name and have schematic variables, this causes problems for Sledgehammer, since it needs to generate some Isar text to refer to the fact.

Thanks for any help.


More information about the isabelle-dev mailing list