On 09.04.2015 21:08, Makarius wrote: > 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. Nice, this deals with the conflict I encountered a few days ago with the use of the \<box> symbol in AutoCorres. > 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. I was not clear above. I don't want to change the general syntax of <position> <to> <rules>, but was contemplating whether the position should read inside-out or outside-in. As I noted in my other mail, this will have to wait for the next round. > 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.) The goal is definitely to have the tool end up in Main, so I will not get too fancy with the syntax.
-- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev