Re: [isabelle] Proof_Context abstraction


a bit of progress:

Am Dienstag, den 29.07.2014, 11:00 +0200 schrieb Joachim Breitner:
> Unfortunately, I get
>         Bad name binding: "local.barfoo"

Tracing existing code a bit more, it seems that I have to go through
Proof_Context.note_thmss, which expects a binding.

So I tried to use Binding.qualified_name to turn the string
local.Cons.IHfoo into a binding. But if I add that using
Proof_Context.note_thmss, "print_facts" will list it as IHfoo, not as


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.