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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
