Fabian and I found the missing check in Cooper's algorithm (src/HOL/Tools/Qelim). The fix can be found in the testboard 52e97a5f5e25. If it works I will push it to the Isabelle repository.
- Johannes Am Samstag, den 01.12.2012, 22:01 +0100 schrieb Florian Haftmann: > In rev. 544764f4324d > > theory Foo > imports Main > begin > > lemma less_dvd_minus: > fixes m n :: nat > assumes "m < n" > shows "m dvd n ⟷ m dvd (n - m)" > using assms apply arith oops > > Florian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
