| #
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
| #
c88d191b |
|
14-Dec-2014 |
blanchet <none@none> |
correctly apply type substitution before checking for function types
|
| #
8994b05e |
|
14-Dec-2014 |
blanchet <none@none> |
avoid generating selectors with function types -- this produce arity inconsistencies
|
| #
ea50fe4a |
|
20-Nov-2014 |
blanchet <none@none> |
work around bug in CVC4, with boolean arguments to (co)datatypes
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
9608121d |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
fd494841 |
|
24-Sep-2014 |
blanchet <none@none> |
allow homogeneous nesting for SMT (co)datatypes
|
| #
80514171 |
|
24-Sep-2014 |
blanchet <none@none> |
interleave (co)datatypes in the right order w.r.t. dependencies
|
| #
899fe76a |
|
24-Sep-2014 |
blanchet <none@none> |
rule out nested (co)recursion for SMT (co)datatypes
|
| #
d9f4cbc7 |
|
24-Sep-2014 |
blanchet <none@none> |
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
|
| #
e3debb98 |
|
17-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
8c52dad5 |
|
17-Sep-2014 |
blanchet <none@none> |
register Isabelle selectors as SMT selectors when possible
|
| #
0695b7e6 |
|
17-Sep-2014 |
blanchet <none@none> |
added codatatype support for CVC4
|
| #
f4f8c25c |
|
17-Sep-2014 |
blanchet <none@none> |
added interface for CVC4 extensions
|
| #
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
|
| #
321ad186 |
|
11-Jun-2014 |
blanchet <none@none> |
use 'ctr_sugar' abstraction in SMT(2)
|
| #
e0f968f4 |
|
11-Jun-2014 |
blanchet <none@none> |
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
|
| #
edea3ba8 |
|
14-Jun-2011 |
boehmes <none@none> |
slightly more general treatment of mutually recursive datatypes;
treat datatype constructors and selectors similarly to built-in constants wrt. introduction of explicit application (in the same way as what is already done for eta-expansion)
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
ead8ec93 |
|
03-Jan-2011 |
boehmes <none@none> |
re-implemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs
|