Re: [isabelle] A small proof checker (String => Bool)

On 25/10/2019 17:07, Juho Kupiainen wrote:
> How could I go about obtaining a small proof checker for Isabelle HOL, that
> takes a theory file and checks that it's valid? I would like it to be
> simple to understand and as few lines of code as possible, yet it should
> include the axioms of the system and be able to check the whole archive of
> formal proofs.

It sound like you ask for an "uninformative green light" for your
theories, but that is neither realistic nor useful.

You need to be more specific about what you mean, and what the
application actually context is. So many things can go wrong. You need
to think about what you want to get right in which way.


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