deal with the case that metis does not time out, but fails instead

reapplied changes to make SML/NJ happy

renaming, minor tweaks, added signature

added signature

moved thms_of_name to Sledgehammer_Util and removed copies, updated references

removed duplicate decleration

made use of sledgehammer_util

renamed sledgehammer_isar_reconstruct to sledgehammer_proof

added comments to new source files

fixed problem with fact names

remove hack and generalize code slightly

simplified isar_qualifiers and qs merging

put shrink in own structure

put annotate in own structure

support assumptions as facts for preplaying

some minor improvements in shrink_proof

some support for ML runtime statistics;

prefer tight Markup.print_int/parse_int for property values;

clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);

eliminated slightly odd identifiers;

tuned syntax, potentially more robust;

smarter list layout;

repaired text following 491c5c81c2e8;

merged

introduce filter_lim as a generatlization of tendsto

merged

based countable topological basis on Countable_Set

qualified interpretation of sigma_algebra, to avoid name clashes

eliminated finite_set_sequence with countable set

support for sub-structured identifier syntax (inactive);

eliminated some improper identifiers;

add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)