doc-src/fixbookmarks.pl
author |
Walther Neuper <neuper@ist.tugraz.at> |
|
Thu, 23 Sep 2010 14:49:23 +0200 |
branch | isac-update-Isa09-2 |
changeset 38014 |
3e11e3c2dc42 |
parent 6636 |
80052270f08b
|
permissions |
-rw-r--r-- |
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 {} \;