[isabelle-dev] New proof method "rewrite"

[Makarius]

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