organized markup properties via apply/unapply patterns;

added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;

ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

merged

tuned code

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;