[isabelle-dev] NEWS: Isabelle sessions and build management

[Peter Lammich]

> Is there really any *need* to have ruby produce theory sources?  Browsing 
> through the outcome briefly, it looks very conventional: a few document 
> antiquotations and a few defininitions/theorems/interpretations issued in 
> Isabelle/ML should do the job.  The bit of Isabelle/ML should be shorter 
> than the ruby stuff.


I hope there is no need. I'm currently working on that issue (and some
related restructuring of the ICF), but it may take some time, as the ICF
and its dependencies are quite large, and my modifications are by far
not backward compatible.


This ruby-script was build as a quick hack to solve the problem of
instantiating generic algorithms for all possible combinations of
implementations. I'm not yet sure what a good solution would be, or
whether one should avoid these instantiations at all, as they seem to be
rarely needed.


Peter