florian.haftmann at informatik.tu-muenchen.de
Wed Apr 18 20:01:59 CEST 2012
> 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 demonstrate interpretations with simultaneous definitions, so that
> we can simply remove it?
Now, there are (IMP). So it is ok that this has gone. It still served
the purpose to remind me of a few things, but these are on my list anyway.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev