> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
