Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Columbo Sample5


view this post on Zulip Email Gateway (Aug 18 2022 at 15:09):

From: Jens Doll <jd@cococo.de>
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 .

Jens
from Ahrensburg, Germany,


Last updated: Nov 21 2024 at 12:39 UTC