[isabelle] Partial Linear Arithmetic
Isabelle now runs on my machine again and I thank Florian for helping me
with the installation. So I was able to enter some simple lemmata and to
rework my verification samples. (Excuse me for the buggy version
beforehand.) I added a third sample
which now contains a more difficult example: the function is rational and
multivariate, but the loop is linear in one variable.
P.S.: I still did not find the correct formula for the modular case,
sample2.html. Isabelle declines to solve the lemma. Does anyone know,
what's wrong there?
This archive was generated by a fusion of
Pipermail (Mailman edition) and