Skolemization support for leo-II and Zipperposition.

document property 'set_induct'

generate 'set_induct' theorem for codatatypes

also try 'metis' with 'full_types'

header tuning

correctly translate THF functions from terms to types

do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

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

tuned;

tuned;

no -optimise -- produces bad bytecode;

output state first -- avoid fluctuation wrt. warnings, errors, etc.;

tuned comment;

updated to polyml-5.5.2-1 which addresses two hard crashes;

updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;

added more functions and lemmas

proper mkdir;

proper option -O;

some reshuffling of Poly/ML version to evade failing tests;

old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;

proper volume name, such that background image is found in /Volumes/Isabelle/.background;

tuned;

tuned message;

setup for drag-and-drop DMG;

merge

reordered provers

compile

faster minimization by not adding facts that are already in the simpset

added missing facts to proof method

don't lose 'minimize' flag before it reaches Isar proof text generation