[isabelle] Columbo Sample5

Hello all,

after my machine had been found corrupted 6 months ago, I had a tough time. Some wicked program switched a key without notifying me and when I noticed that, 4 months of work had been lost. Now I managed to recover my project without external help and was able to have Columbo automatically verify a program, which computes the first terms of the sine. A lot of algebra and reduction technique is involved in the sample http://www.cococo.de/products/windows/Columbo/sample5.html and I would be grateful for comments and suggestions. Also an older example, the symbolic newton method, has been updated http://www.cococo.de/products/windows/Columbo/sample4.html .

from Ahrensburg, Germany,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.