infrastructure for extraction of equations x = t from premises beneath meta-all

--HG--
extra : rebase_source : 8bcc91c27655c862caf8a5c7a310c2b0e1cf2064

proper context;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

eliminated aliases;

tuned signature;
clarified context;

simplifier uses proper Proof.context instead of historic type simpset;

simplified Data signature;

misc tuning and simplification;

misc tuning;

do not open ML structures;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;

modernized structure Proof_Context;

now works for schematic terms as well, thanks to Alex for the `how-to'

typos in comment

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

removed old CVS Ids;
tuned headers;

fine-tuned elimination of comprehensions involving x=t.

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

Goal.prove: context;

Goal.prove;

simprocs: Simplifier.inherit_bounds;

Deleted Library.option type.

adapted type of simprocs;

use Tactic.prove instead of prove_goalw_cterm in internal proofs!

now permutations of quantifiers are allowed as well.

generalization of 1 point rules for ALL

added simproc for bounded quantifiers

Fixed a bug in the EX simproc.

Quantifier elimination procs.