Re: [isabelle] Large theories





On 08/06/2016 15:01, ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ wrote:
Dear Tobias and Makarius!
Thank you for your links and suggestions.

Now I realize that it's better to import my objects to ML directly. I will
concentrate on this approach.

I have a question regarding "eval" proof method.
If one uses "eval", what stack of code will one have to trust? Will the "trusted
base" be larger than that for proofs without "eval"?

Yes, you also need to trust the translation of HOL function definitions into ML function definitions.

Tobias

If you can give any links discussing the topic of trusted code stack in theorem
provers (whether in case of "eval" method or not) â I would appreciate it.

Thank you!
Stanislav.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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