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
> Classical.put_global_claset?

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).


	Makarius





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