[isabelle] Slots for diagnostic value command



In 4044a7d1720f, there was a change: the ancient »slots« for value
(code, nbe, simp) and the default behaviour of sequential trys have been
given up in favour of one hard-coded behaviour:
* If the term to evaluate does not contain free variables, evaluate
using ML.
* If the term contains free variables or the first step fails, evaluate
using nbe.

Recent experience suggests that this step was maybe too rigorous since
»value« is also used for purposes beyond diagnostic evaluation which
demand a more predictable behaviour, esp. wrt. ongoing developments of
theories.

My suggestion would be to revive the »slots« as follows:
* Slot »default« implementents the current behavior and is the default.
* The former slots (s.a.) are restored again.

Any comments?

This is something I definitely do not promote for the approaching
release, but rather for its successor.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.