[isabelle-dev] adhoc overloading

Makarius makarius at sketis.net
Fri Jul 12 17:00:40 CEST 2013


On Fri, 12 Jul 2013, Christian Sternagel wrote:

> The patches should be ready to push (for your convenience I attached them 
> once more; the attached patches are the same as from my previous e-mail). 
> Btw, I generated the patches against Isabelle 8afb396d9178 and AFP 
> 908304753f7d (but I guess this information is also included in the patches 
> ;)).

This is now Isabelle/e0ff1625e96d and AFP/74746c992248.  Since you did not 
provide formal changesets, only diffs, I invented some log messages on the 
spot.  (Normally I use the "hg export" / "hg import" pair for small-scale 
patch-flow, but "hg import" was happy importing plain diffs like this.)

I added Isabelle/fee0db8cf60d to keep the generated Proof General keyword 
tables in sync.  This is now trivial with the "isabelle update_keywords" 
tool in its fully static version.  (In the past there was always a full 
build required before applying it, or a good guess which sessions 
contribute to the keyword tables.)


 	Makarius



More information about the isabelle-dev mailing list