#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
75c0bb14 |
|
13-Aug-2016 |
blanchet <none@none> |
killed final stops in Sledgehammer and friends
|
#
185dcd47 |
|
02-Apr-2016 |
wenzelm <none@none> |
prefer infix operations;
|
#
b09f23e4 |
|
27-Mar-2016 |
blanchet <none@none> |
early warning when Sledgehammer finds a proof
|
#
dccdabe3 |
|
03-Mar-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
1971a62a |
|
13-Aug-2015 |
wenzelm <none@none> |
tuned signature, in accordance to sortBy in Scala;
|
#
3045319d |
|
20-Nov-2014 |
blanchet <none@none> |
other way of crashing (with CVC4)
|
#
f6662567 |
|
25-Apr-2015 |
blanchet <none@none> |
made CVC4 support work also without unsat cores
|
#
76c7446c |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued obsolete Output.urgent_message;
|
#
21bbd523 |
|
30-Sep-2014 |
blanchet <none@none> |
tuned output in case of one-liner failure
|
#
ac75f5e7 |
|
27-Aug-2014 |
blanchet <none@none> |
renamed new SMT module from 'SMT2' to 'SMT' --HG-- rename : src/HOL/SMT2.thy => src/HOL/SMT.thy rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML
|
#
b5f6d801 |
|
12-Jun-2014 |
blanchet <none@none> |
removed dead code
|
#
4ad40712 |
|
12-Jun-2014 |
blanchet <none@none> |
reintroduced vital 'Thm.transfer'
|
#
998aa7d7 |
|
23-May-2014 |
blanchet <none@none> |
removed noise
|
#
312fdfa6 |
|
21-May-2014 |
blanchet <none@none> |
tuning
|
#
0798791c |
|
16-May-2014 |
blanchet <none@none> |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
#
52dd9fc9 |
|
27-Mar-2014 |
wenzelm <none@none> |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
#
f936bab5 |
|
13-Mar-2014 |
blanchet <none@none> |
integrate SMT2 with Sledgehammer
|
#
cf3941c9 |
|
13-Feb-2014 |
blanchet <none@none> |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
#
a2e9e36e |
|
03-Feb-2014 |
blanchet <none@none> |
properly overwrite replay data from one compression iteration to another
|
#
9a5b75f2 |
|
03-Feb-2014 |
blanchet <none@none> |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
#
62d265e3 |
|
03-Feb-2014 |
blanchet <none@none> |
added 'smt' option to control generation of 'by smt' proofs
|
#
700f2e9d |
|
03-Feb-2014 |
blanchet <none@none> |
renamed ML file --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML => src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
|
#
94e4af3c |
|
03-Feb-2014 |
blanchet <none@none> |
merged 'reconstructors' and 'proof methods'
|
#
fed5d9bd |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
#
945bedcb |
|
31-Jan-2014 |
blanchet <none@none> |
moved ML code around
|
#
06f3d979 |
|
30-Jan-2014 |
blanchet <none@none> |
refactor large ML file
|