Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] which library should be imported in order to p...

Email Gateway (Aug 22 2022 at 10:38):

From: Mandy Martin <tesleft@hotmail.com>
Hi ,
which library should be imported in order to prove these
Lemma GCD(A,B) -> A+BLemma Min(A,B) -> Max(A,B)
where A,B are algebra, i do not know the criteria of A and B, would like to find which cases can make lemma above valid and which case is invalid and can auto prove it or how to prove.
Regards,
Martin

Last updated: Apr 24 2024 at 12:33 UTC