Re: [isabelle] Proof_Context abstraction



Hi,

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
Cons.IHfoo.



Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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