tune slices further

tweak ATP slices further

compile

also have SMT solvers alternate fact filter

use the right filter in each slice

tuned slices

store fact filter along with ATP slice

tuned data structure

thread through fact triple component from which used facts come, for accurate index output

more precise output of selected facts

thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices

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;