|
From: | daniel |
Subject: | Re: [Isarmathlib-devel] A contribution |
Date: | Sat, 8 Sep 2012 12:23:16 +0200 |
User-agent: | Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:15.0) Gecko/20120824 Thunderbird/15.0 |
I did some more work. From now on, the
web page you should check for my
files is just: https://belenus.unirioja.es/~daconcep/ The real numbers are not so easy to work with, the metric spaces need some rewriting. In the case of the partitions, I tried to work with the existing definition, but my skills with this kind of functions is very limited. I'm used to HOL. By the way, in the context real0 and real1 there is mistake (copy-paste, I guess). The "minus" for reals and integers have the same name for their definition rule (rminus_def). I guess on the integers was supposed to be "iminus_def". Daniel
|
[Prev in Thread] | Current Thread | [Next in Thread] |