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