Re: [isabelle] Replacing COMP



On Thu, 1 Aug 2013, René Neumann wrote:

I'd like to point out though, that I do not use Isabelle/ML and hence
the point (as I understand you), that using it in ML without thought
might deal some harm, does not apply here. Or could it really deal some
damage in the high-level view I'm using?

We did not get very far so far, the thread is going backwards in circles.

Andreas Lochbihler made several constructive attempts to guess what you are trying to do and propose some alternatives. Maybe you can show more of the actual application, so that it can be sorted out the proper way.


I do trust you that there are good reasons to remove COMP.

Just normal garbage collection on the sources: it was no longer used and in conflict with certain concepts, causing occasional breakdown in unexpected situations, so it was deleted. This time it was not about "old-fashioned" or "legacy" features, but obsolete things as the NEWS explained that. If it would have been non-obsolete, I would have had to sit down and think about getting 8 variants of COMP into Isar source language.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.