# [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
http://cococo.de/products/windows/Columbo/sample3.html
which now contains a more difficult example: the function is rational and
multivariate, but the loop is linear in one variable.
Jens
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
MHonArc.*