updated Knowledge/Biegelinie.thy

updated Knowledge/EqSystem.thy

intermediate state in Knowledge/EqSystem.thy

updated Knowledge/Integrate.thy

updated Knowledge/DiffApp.thy

tuned

src/Knowledge + test/Knowledge:
find . -type f -exec sed -i s/"f_\""/"f_f\""/g {} \;
find . -type f -exec sed -i s/"f_,"/"f_f,"/g {} \;
find . -type f -exec sed -i s/"f_:"/"f_f:"/g {} \;
find . -type f -exec sed -i s/"f_'_"/"f_f'"/g {} \;
find . -type f -exec sed -i s/"eqs_"/"eqs"/g {} \;
find . -type f -exec sed -i s/"f'_ "/"f_f' "/g {} \;
find . -type f -exec sed -i s/"f'_)"/"f_f')"/g {} \;

updated Knowledge/Diff.thy

updated Vect..LogExp.thy

in src/Knowledge + test/Knowledge:
find . -type f -exec sed -i s/"e_]"/"e_e]"/g {} \;

tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \;

tuned