updated Knowledge/RootEq.thy

changed argument types for scripts

find . -type f -exec sed -i s/'real_list_'/'REAL_LIST'/g {} \;
find . -type f -exec sed -i s/'real_set_'/'REAL_SET'/g {} \;
find . -type f -exec sed -i s/'real_ '/'REAL '/g {} \;
find . -type f -exec sed -i s/'real_real_'/'REAL_REAL'/g {} \;

find . -type f -exec sed -i s/'bool_list_'/'BOOL_LIST'/g {} \;
find . -type f -exec sed -i s/'bool_'/'BOOL'/g {} \;

corrected format for axioms in remaining theories

updated Knowledge/Root.thy, plus changes ahead.

find . -type f -exec sed -i s/'left_diff_distrib2'/'right_diff_distrib'/g {} \;
find . -type f -exec sed -i s/' typ_ord'/' Term_Ord.typ_ord'/g {} \;
find . -type f -exec sed -i s/' term_ord'/' Term_Ord.term_ord'/g {} \;

updated Knowledge/Equation.thy, plus changes ahead.

find . -type f -exec sed -i s/' e_\"'/' e_e\"'/g {} \;
find . -type f -exec sed -i s/' e_ '/' e_e '/g {} \;
find . -type f -exec sed -i s/' e_)'/' e_e)'/g {} \;
find . -type f -exec sed -i s/' e_,'/' e_e,'/g {} \;
find . -type f -exec sed -i s/' e_:'/' e_e:'/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 {} \;
find . -type f -exec sed -i s/' v_)'/' v_v)'/g {} \;
find . -type f -exec sed -i s/' v_,'/' v_v,'/g {} \;
find . -type f -exec sed -i s/' v_:'/' v_v:'/g {} \;

find . -type f -exec sed -i s/' v_i\"'/' v_i\"'/g {} \;

updated Knowledge/PolyMinus, plus some changes ahead

updated Knowledge/Rational

renamed
find . -type f -exec sed -i s/discard_minus_/discard_minus1/g {} \;
find . -type f -exec sed -i s/discard_parentheses_/discard_parentheses1/g {} \;
TODO: reconsider naming of similar rls

intermediate state Knowledge/Rational.ML, optimizing reading error msg

impl. parse_patt into fun prep_pbt, prep_met

updated Poly.thy finally: introduced "fun parse_patt"

When introducing ctx's in the future, one can search for thy2ctxt !