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 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.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
