[isabelle-dev] HOL/ex/Set_Algebras

[Alexander Krauss]

Hi all,

while backporting HOL/Library/Set_Algebras to use type classes again (a 
remaining point of the 'a set transition), I noticed that there is now a 
clone of that file in HOL/ex. The changelog says:

> changeset:   41581:c34415351b6d
> user:        haftmann
> date:        Sat Jan 15 20:05:29 2011 +0100
> summary:     experimental variant of interpretation with simultaneous definitions, plus example

Unfortunately, nothing in the file itself states what it should 
demonstrate. Instead, the original comments remain, so there is plenty 
of opportunity for getting totally confused.

What should we do with the clone? Are there maybe other examples that 
can demonstrate interpretations with simultaneous definitions, so that 
we can simply remove it?

Alex