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
This archive was generated by a fusion of
Pipermail (Mailman edition) and