Hi Tjark,
some comments in addition to Clemens':
* The documentation for local specification mechanisms is not very
homogeneous. The tutorials on type classes and locales are valuable.
From a user's perspective, however, a unifying discussion (with guidance
on when to use which) is missing.
Clemens,
Thanks for your quick reply!
On Thu, 2010-12-16 at 20:37 +0100, Clemens Ballarin wrote:
Suggestions? The message also says that the relation is probably not
terminating.
Well, roundup bound is developer jargon. Sublocale relation probably
not terminating points into the right
On Fri, 17 Dec 2010, Tjark Weber wrote:
One could think about (tool support for) formally checked hyperlinks
from ML sources into LaTeX (and other) documents.
We have been moving towards that for several years. At least the manuals
maintained by myself contain many formally checked
I've recently worked on an algebraic hierarchy, ranging from semi-groups
to Kleene algebras and related structures, in Isabelle/HOL. It goes
without saying that Isabelle's local specification mechanisms were well
suited for the task. However, using classes and locales more
extensively for the
