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 moment.

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.


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to