On Fri, 7 May 2010, Brian Huffman wrote:
I am looking for some advice on a design decision for the HOLCF fixrec
package.
Fixrec uses the simplifier when doing its internal proofs of the
defining equations for a function. Currently it maintains its own
special simpset for this purpose, which users can extend by declaring
theorems with the [fixrec_simp] attribute. The alternative would be to
get rid of [fixrec_simp] and just use the main simpset from the theory
context (i.e. theorems declared with [simp]).
Just a technical note on this: the "main simpset" is the one from a
regular local context, which can be retrieved via the regular Operation
simpset_of: Proof.context -> simpset
The non-standard variant global_simpset_of: theory -> simpset is there for
old tools that do not have a proper context available. There is also some
system infrastructure that needs such global operations to initialize a
certain context.
Tools and packages that have already been localized, and fixrec appears to
be one of them, should never refer to "global" stuff from the raw
background theory.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
