merged

improved readability

tweaked calculation of sledgehammer messages

adapted sledgehammer warnings

fixed case split preplaying

fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup

preplay case splits

added warning when shrinking proof without preplaying

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;