[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 MHonArc.