Re: [isabelle] Large theories

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"?

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!

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