[isabelle] src/HOL/Library/Eval_Witness.thy

Are there any existing applications of this theory?

It has once (6 years ago) been the elaboration of an innovative idea but
I have almost forgotten about it.  In the presence of generated abstract
datatypes, I think it is not even valid any longer.

At least I would suggest to move it to ex/, or drop it entirely.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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