makarius at sketis.net
Thu Oct 11 17:35:04 CEST 2012
On Thu, 11 Oct 2012, Florian Haftmann wrote:
>> The class_deps non-scalability probably stems from the omission of the
>> transitive reduction (Hasse diagram). This was probably done due to the
>> anticipated locale graph visualization (which does not quite work), or
>> it might be just an omission.
> The latter. I am not aware of any locale graph visualization apart from
> a sketch two (?) years ago on the mailing list.
The result is called Graphview now. The 'locale_deps' command will give
you the locale aspect of it, but the result is not very usable at the
A side question here: Is there a sensible way to make 'print_locale'
informative about its axiomatic basis, or its view in terms of the goal
presented in interpretation.
See also changeset 7b6aaf446496, where I trashed your earlier attempt at
it without looking very closely at it -- the priority was to unify the
pretty output / pretty tooltip model and get rid of hardwired "locale"
content of the graphview tool.
More information about the isabelle-dev