[isabelle-dev] Set_Algebras: Overloading + on 'a set (again)

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120104/46c6ffc5/attachment.sig>