src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
2017-06-06 wenzelm 2017-06-06 discontinued obsolete print mode;
2015-11-30 blanchet 2015-11-30 avoid 'hence' and 'thus' in generated proofs
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-09-29 blanchet 2014-09-29 make sure no '__' suffixes make it until Isar proof
2014-09-29 blanchet 2014-09-29 rename skolem symbols in the negative case as well
2014-08-28 blanchet 2014-08-28 use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
2014-08-28 blanchet 2014-08-28 generate 'thesis' variable in Sledgehammer Isar proofs
2014-08-28 blanchet 2014-08-28 three-line 'obtain' format for generated Isar proofs
2014-08-28 blanchet 2014-08-28 reintroduced two-line-per-inference Isar proof format
2014-08-05 blanchet 2014-08-05 tuned skolemization
2014-08-05 blanchet 2014-08-05 rationalize Skolem names
2014-08-04 blanchet 2014-08-04 rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-01 blanchet 2014-08-01 better handling of variable names
2014-08-01 blanchet 2014-08-01 nicer generated variable names
2014-07-25 blanchet 2014-07-25 more robustness in Isar proof construction
2014-07-24 blanchet 2014-07-24 introduce fact chaining also under first step
2014-06-24 blanchet 2014-06-24 given two one-liners, only show the best of the two
2014-06-24 blanchet 2014-06-24 don't generate Isar proof skeleton for what amounts to a one-line proof
2014-06-02 fleury 2014-06-02 basic setup for zipperposition prover
2014-05-16 blanchet 2014-05-16 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 blanchet 2014-05-16 use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-03-13 blanchet 2014-03-13 integrate SMT2 with Sledgehammer
2014-02-03 blanchet 2014-02-03 don't lose additional outcomes
2014-02-03 blanchet 2014-02-03 generate comments in Isar proofs
2014-02-03 blanchet 2014-02-03 renamed ML file
2014-02-03 blanchet 2014-02-03 merged 'reconstructors' and 'proof methods'
2014-02-03 blanchet 2014-02-03 added 'smt' as a proof method
2014-02-03 blanchet 2014-02-03 tuning
2014-02-03 blanchet 2014-02-03 refactor relabeling code
2014-02-03 blanchet 2014-02-03 tuned data structure
2014-02-03 blanchet 2014-02-03 tuned data structure
2014-02-03 blanchet 2014-02-03 more flexible compression, choosing whichever proof method works
2014-02-02 blanchet 2014-02-02 more data structure rationalization
2014-02-02 blanchet 2014-02-02 rationalized threading of 'metis' arguments
2014-02-02 blanchet 2014-02-02 simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
2014-01-31 blanchet 2014-01-31 generalized preplaying infrastructure to store various results for various methods
2014-01-31 blanchet 2014-01-31 added a 'trace' option
2014-01-31 blanchet 2014-01-31 moved code around
2014-01-31 blanchet 2014-01-31 added 'algebra' to the mix
2014-01-31 blanchet 2014-01-31 more informative trace
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 more concise Isar output
2014-01-31 blanchet 2014-01-31 better tracing + syntactically correct 'metis' calls
2014-01-31 blanchet 2014-01-31 tuned ML function names
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 moved ML code around
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure