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`
gives
*** 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.
Jasmin
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
