* Generic Toplevel.add_hook interface allows to analyze the result of
transactions (including failed ones). For example, see
src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency
output of transactions resulting in a new theory state.
* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
formalized as type Name.binding, replacing old bstring.
INCOMPATIBILITY, need to wrap strings via Name.binding function, see
also Name.name_of. Packages should pass name
On Tue, 2 Sep 2008, David Aspinall wrote:
> > You can achieve the above "name space effect" of symbols already via
> > something like \,
>
> Aha -- we can easily do this in PG then instead of \.
>
> > which is presently unused because LaTeX output is a bit strange (as for
> > \).
>
> The idea
On Tue, 2 Sep 2008, David Aspinall wrote:
> \
>
> \
>
> This is already supported in the X-Symbol replacement in the CVS version of
> Proof General, by the way, although Isabelle's lexer currently only allows
> syntax like \ and \.
The \ notation is more fundamental, below lexing even. It
> You can achieve the above "name space effect" of symbols already via
> something like \,
Aha -- we can easily do this in PG then instead of \.
> which is presently unused because LaTeX
> output is a bit strange (as for \).
The idea is to make the output the same as \, of course (with the
inions?
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL:
<https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080902/d526bc4b/attachme
> There have been some thoughts to provide a mechanism of overloaded
> abbreviations or something similar to eliminate that problem
Yes --- I think the simplest thing is to simulate overloading by
extending Isabelle symbols with symbol variants, which automatically
have the same appearance but
Quoting Florian Haftmann :
> * funpow is defined as a separate primrec in theory Nat, without special
> syntax.
> * The remainder of theory Relation_Power is moved to Library, with a new
> infix syntax (e.g. "^^") for relpow.
> * The simple pow "^" then is just a primrec in class comm_monoid_mult
