[isabelle-dev] PG preferences (auto solve in particular)

Florian Haftmann 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.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091111/4616a7ee/attachment.sig>

More information about the isabelle-dev mailing list