[isabelle] Verify the legitimacy of a proof?



Hi All,

Let's suppose I have some lemma

lemma ComplexProperty: "something interesting"
...
done

whose proof cites numerous other lemmas in other .thy files, possibly
written by other persons with malicious intentions. Is there a command in
Isabelle which I could use to determine the legitimacy of the entire proof
tree of ComplexProperty? That is, I want to ensure that no lemma in the
proof tree ended with "sorry", or if any axioms were used, I want to know
which ones, etc.

Thanks,

Scott Constable



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