[isabelle-dev] PG preferences (auto solve in particular)
florian.haftmann at informatik.tu-muenchen.de
Wed Nov 11 09:17:19 CET 2009
I'm currently asking myself whether the substructure of Isabelle
settings in the preferences menu is already carved in stone (although
only some adventurous people seem to be using PG 4 by now).
In my naive view the distinction between "Display" and "Advanced
display" is quite artifical, whereas things like "Auto solve" and "Auto
nitpick" should be better placed in a separate menu "Hints". Or is
there a rationale I am not aware of for the current categorization?
It is well-known that autosolve sometimes struggles with unification,
e.g. in Record.thy, lemma
istuple_update_swap_fst_fst. I do not know either whether there have
been any ideas around how this trap could be circumvented, but my own
experience suggests we should definitely try.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 260 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev