Re: [isabelle] Pitfall with type-classes in Isar-Lemma format
> Is this just an exercise in driving the system into an unspecified /
> uninhabitable state, or does it have some practical significance?
I have distilled that from a practical example, that went like this:
notes [refine_transfer] = <Some lemmas that only makes sense for this
particular refinement proof>
shows "?concrete_program <= abstract_program"
by (tactic that uses lemmas declared with attribute
"refine_transfer" (which is a NamedThms structure)
As I do not know how to refer to the schematic
variable ?concrete_program when I do
proof - note [refine_transfer] = ... show "xxx" ...
(For xxx, neither ?thesis nor "?concrete_program <= abstract_program"
I used the notes-syntax.
An alternative would be to pass the lemmas as parameters to my tactic,
which I have already (partially) implemented (after writing the first
mail ;) ).
This archive was generated by a fusion of
Pipermail (Mailman edition) and