[isabelle-dev] Presburger proof term

[Tobias Nipkow]

All of the lemmas involved are either arihmetic or logical inference 
rules and make sense. Presburger is a generic and complex decision 
procedure. I am not surprised and would not want to optimize presburger 
to use fewer lemmas.

Tobias

Am 28/06/2011 00:08, schrieb 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
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev