> Here is another change to be considered in the project of 'a set recovery: > > changeset: 26814:b3e8d5ec721d > user: berghofe > date: Wed May 07 10:59:24 2008 +0200 > files: src/HOL/Library/BigO.thy > src/HOL/Library/SetsAndFunctions.thy src/HOL/MetisExamples/BigO.thy > description: > Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with > definitions of + and * on functions. > > This is a result from inspection of "hg log -u berghofe -r > Isabelle2007:Isabelle2008". I have already reverted a few more obvious > things in c296c75f4cf4.
This indeed is what is mentioned as »backport theory Set_Algebras to
type classes« on the list open issues.
Florian
--
Home:
http://www.in.tum.de/~haftmann
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
