Hi Alex,
while backporting HOL/Library/Set_Algebras to use type classes again (a
remaining point of the 'a set transition),
thanks for doing this!
I noticed that there is now a
clone of that file in HOL/ex.
What should we do with the clone? Are there maybe other examples that
can
Hi Florian,
Thanks for the clarification.
Its purpose
might have been to make the interpretation notationally simpler.
the story behind is not about syntax. It is really about the
simultaneous definitions. For a motivation, you can have a look at the
tutorial on code generation, section
I wondered when somebody would ask this. What's going on here is a
hack, and I'm not very happy about it.
If you follow up the imported theory, you will find some code that
provides a clone of the interpretation command (under the same name!)
with some added functionality (definitions).
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
