On Thu, 9 Apr 2015, Lars Noschinski wrote:
On 18.03.2015 15:16, Lars Noschinski wrote:
commit 4ed50ebf5d36 adds a new proof method "rewrite". This is the
pattern-based replacement for subst Christoph Traut and I presented at
the last Isabelle Workshop [1]. For now, it lifes in
~~/src/HOL/Library/Rewrite and is still missing a proper documentation
(but there are examples in ~~/src/HOL/ex/Rewrite_Examples).
I've used it now a bit to add annotations in program verification and
(contrary to my former intuition) found the order of the patterns to be
the wrong way around.
If someone has used the rewrite method and has some opinions on that, I
would be glad to hear these.
I haven't used it yet, although I looked a bit through the sources, just
as a matter of pre-release routine.
I also added a symbol assignment for \<hole> in the IsabelleText font and
isabellesym.sty -- it is the result of spending 30min looking carefully
through DejaVuSansMono and
http://mirrors.ctan.org/info/symbols/comprehensive/symbols-a4.pdf -- see
now b911c8ba0b69. LaTeX packages should not be overly exotic as rendering
of Isabelle symbols -- hopefully wasysym.sty was a decent choice here.
Back to the actual topic of this thread: If you want to change the syntax
for the release, there are a very few days left until the first release
candidate is published, while the repository still remains in pre-forked
state, probably until the end of next week.
Technically, to have Parse.xthms1 before quasi-keywords like "at", you
need some Scan.unless trickery, but it should be doable. Method.sections
also manages that with "add", "del" etc.
Here is also a command line to explore possibilities of true keywords,
instead of quasi-keywords:
$ isabelle build -n -a -d '$AFP' -k at -k asm -k concl
Note that outer syntax is now local to each theory, so as long as it is
just a separate theory somewhere, one can be liberal. Anything for main
HOL needs more care, of course. (For Eisbach we also have some open
problems with keyword clashes still left to address, "concl" is one of
them.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
