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

Makarius makarius at sketis.net
Wed Jan 4 11:25:42 CET 2012


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.


 	Makarius


More information about the isabelle-dev mailing list