2014-06-02 ago basic setup for zipperposition prover
2014-05-16 ago correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 ago use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-03-13 ago integrate SMT2 with Sledgehammer
2014-02-03 ago don't lose additional outcomes
2014-02-03 ago generate comments in Isar proofs
2014-02-03 ago renamed ML file
2014-02-03 ago merged 'reconstructors' and 'proof methods'
2014-02-03 ago added 'smt' as a proof method
2014-02-03 ago tuning
2014-02-03 ago refactor relabeling code
2014-02-03 ago tuned data structure
2014-02-03 ago tuned data structure
2014-02-03 ago more flexible compression, choosing whichever proof method works
2014-02-02 ago more data structure rationalization
2014-02-02 ago rationalized threading of 'metis' arguments
2014-02-02 ago simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
2014-01-31 ago generalized preplaying infrastructure to store various results for various methods
2014-01-31 ago added a 'trace' option
2014-01-31 ago moved code around
2014-01-31 ago added 'algebra' to the mix
2014-01-31 ago more informative trace
2014-01-31 ago tuning
2014-01-31 ago more concise Isar output
2014-01-31 ago better tracing + syntactically correct 'metis' calls
2014-01-31 ago tuned ML function names
2014-01-31 ago tuning
2014-01-31 ago moved ML code around
2014-01-31 ago renamed many Sledgehammer ML files to clarify structure