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

[Lawrence Paulson]

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.

Larry