On Wed, Aug 17, 2011 at 11:51 AM, Florian Haftmann
wrote:
> HOLCF-Library FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/c478cd500dc4
> HOL-Bali FAILED
> HOL-Decision_Procs FAILED
> HOL-Induct FAILED
> HOL-Subst FAILED
> HOL-NanoJava FAILED
Fixed: http://isabelle.in.tum.de/repos/isabe
Hi all,
I repeatedly stumble over duplication among the Isabelle distribution
and the AFP, c.f.
Library/AssocList.thy
and
http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/BytecodeLogicJmlTypes/AssocLists.thy
Complete_Lattices.thy
and
http://afp.hg.sourceforge.net/hgweb/afp/afp/
[forgot to answer in particular]
> inquit Brian:
>> As long as we put off reintroducing 'a set as a separate type, we will
>> continue to accumulate more theories (like Multivariate_Analysis) that
>> confuse sets and predicates. The job of introducing 'a set will only
>> get more difficult the lon
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 prop
Hi again,
inquit Brian:
> Overall, I must say that I am completely in favor of making set a
> separate type again. But I also believe that the sets=predicates
> experiment was not a waste of time, since it forced us to improve
> Isabelle's infrastructure for defining and reasoning about predicates