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
foo
Description: Binary data
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
