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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
