another attempt to standardize sort order in a portable way;

rebundled polyml-5.5.0-2, which now includes the sources as usual (e.q. required for formal references in Isabelle/ML);

updated for release;

tuned;

minimal updated of jEdit/README.html, without any substantial reforms;

clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;

avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;

report status more frequently on demand;

more efficient inlined properties, especially relevant for voluminous tasks trace;

more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);

repackaged polyml-5.5.0-1 -- only x86-cygwin changed;

better apply peflags at build time, to avoid antivirus getting nervous about changing executables;

Added tag Isabelle2013-RC1 for changeset 2c3d0cb151c0

tuned state display

tuned names

tuned

tuned identifier

tuned top

Typo in description of abs_def.

distinguish one more kind of proofs

added markers in proofs identifying origin of proofs, in eval driver

added option to use SNoW as machine learning algo

more robustness in Isar proof reconstruction (cf. bug report by Ondrej)

more precise error message

killed deadcode

more robustness w.r.t. 0

hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly

tuned indent

drop needless .0s

distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation

infix syntax for streams (reflecting the one for lists)

replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules

check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop

removed spurious trimming

tuned

tuned slicing (E-MaLeS and E-Par)

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;