[isabelle-dev] Presburger proof term

[Jasmin Blanchette]

Hi all,

Quick question: Josef Urban noticed that the proof terms for some lemmas proved directly by "presburger" can refer to lots of other lemmas; for example, the proof of "Parity.even_mult_two_ex" directly refers to 206 lemmas.

ML {* Thm.proof_body_of @{thm Parity.even_mult_two_ex} *}

(I've attached the list.) Is that normal? Does this have anything to do with "presburger"?

Jasmin

-------------- next part --------------
A non-text attachment was scrubbed...
Name: foo
Type: application/octet-stream
Size: 4319 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110628/0bd28ed9/attachment-0001.obj>