krauss at in.tum.de
Thu Apr 12 20:06:14 CEST 2012
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?
More information about the isabelle-dev