quotient package: deal correctly with frees in lifted theorems

approximation_oracle: actually match true/false in ML, not arbitrary values;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more precise Command.State accumulation;

eliminated some old camel case stuff;

some attempts to recover Isabelle/ML style from the depths of time;

keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;

select tangible text ranges here -- more robust against ongoing changes of the markup query model

structure Thm: less pervasive names;

discontinued obsolete 'global' and 'local' commands;