Re: [isabelle] Creating new Isar theorem attributes
On Mon, 28 Nov 2005, John Matthews wrote:
> The isar.thy file installs the new theorem attribute, and isar_test.thy
> tries to use it. I've instrumented the theorem attributes with "print"
> instructions, but none of them seem to fire.
Oddly, there seems to be something wrong with print being used here --
maybe the compiler removes this from encapsulated toplevel expressions.
I do use PolyML.print regularly, but usually from actual ML files, rather
than immediate ML code as encountered here. Using Isabelle's own functions
does work, e.g. warning or writeln.
I also see your solver stemming from the D2 rule in the claset.
Also note that attribute names quoted in a theory need to conform to the
identifier syntax given in the isar-ref manual. This is quite liberal,
but does not include a bang as part of a word. The attributes in
Provers/classical.ML do this by parsing there own arguments (cf.
occurences of Args.bang, Args.bang_colon).
> Also, what is the difference between "local" and "global" theorem
> attributes? That is, when should I use Classical.put_local_claset versus
Attributes operate either in a theory (global) of proof context (local). A
global attribute should change the theory -- there is no proof context
available anyway, a local attribute should change the proof context (in
purely functional manner).
This archive was generated by a fusion of
Pipermail (Mailman edition) and