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 {} \;
3 # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
5 # requires some GNU tools
20 ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
22 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
24 TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
25 FILELOC="${LOC:${#ISABELLE_SRC}}"
26 if [ "$TITLE" != "$FILELOC" ]
28 if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
30 if [ -n "$ONLY_FILENAMES" ]
32 echo "Inconsistency in $LOC: $TITLE"