Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

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

[isabelle-dev] Isabelle and AFP

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/

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[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

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

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

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

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