[isabelle] Verify the legitimacy of a proof?
Let's suppose I have some lemma
lemma ComplexProperty: "something interesting"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and