simplified SMT solver code in Sledgehammer

eliminated needless speed optimization -- and simplified code quite a bit

distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds

report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices

remove unnecessary assumption from real_normed_vector

adapted to new MaSh interface

use order topology for extended reals

introduce order topology

simplify heine_borel type class

compute proper weight for "p proves p" in MaSh

restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual

tuned

back to post-release mode -- after fork point;

updated for release;

merged

misc tuning for release;

tuned;

accomodate scala-2.9.2;

afford parallel proof terms;

always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;

simplified proofs

tuning

misc cleanup;

tuned signature;