Hi Florian,
Am 18.08.2011 um 09:18 schrieb Florian Haftmann:
@list: btw. what is the status of »refute« in general? Is it supposed
to be superseded by nitpick entirely?
Pretty much so, yes, but there are a few reasons why I would rather that we
keep it around:
1. Refute participates at
On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote:
The maintenance load is extremely low. When it comes to the REFUTE
exception, I can look at it if and when we decide to move back to
sets.
I suspect that Jasmin will have no trouble fixing this, but otherwise
I'd be happy to
Hi again,
thanks to all contributors who already started to sort out some of the
set-pred mixture issues.
I have merged recent changes back into
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ -- this
is meant as a mere basis for figuring out problems experimentally, not
as a
On 11/08/2011, at 2:44 PM, Florian Haftmann wrote:
Then the following sessions fail:
HOL-Algebra
HOL-Auth
HOLCF
HOL-ex
HOL-Hahn_Banach
HOL-Hoare_Parallel
HOL-IMP
HOL-Imperative_HOL
HOL-Induct
HOL-Library
HOL-Matrix
HOL-Metis_Examples
HOL-MicroJava
Hi again,
as feasibility study I re-introduced the good old set type constructor
at a recent revision in the history. The result can be inspected at
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329
This is by no means meant as a thorough treatment of the whole
