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

Lawrence Paulson lp15 at cam.ac.uk
Tue Aug 23 13:51:09 CEST 2011

I'm starting to have doubts about this entire procedure.

I thought the plan was to get these theories (particularly in the AFP) into a state where they no longer dependent on confusing sets with predicates so that they would work with either version of Isabelle. I'm not sure that's possible. I got DataRefinementIBP working with the set-version, but now it doesn't work with the standard version. For one thing, it needs a class declaration for type set, which obviously cannot work with the standard version, but other proofs also fail to work with the standard version.

I don't think it's possible to have it both ways. We need to either say we are making this change (and then pushing it through) or not making this change.


More information about the isabelle-dev mailing list