updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
29 ^doc-src/.*\.tex.backup
35 ^src/Tools/jEdit/nbproject/private/
36 ^src/Tools/jEdit/build/
37 ^src/Tools/jEdit/dist/
38 ^src/Tools/jEdit/contrib/