blanchet [Fri, 22 Oct 2010 13:54:51 +0200] rev 40067
renamed files
blanchet [Fri, 22 Oct 2010 13:49:44 +0200] rev 40066
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
blanchet [Fri, 22 Oct 2010 13:48:21 +0200] rev 40065
remove more needless code ("run_smt_solvers");
tuning
blanchet [Fri, 22 Oct 2010 12:15:31 +0200] rev 40064
got rid of duplicate functionality ("run_smt_solver_somehow");
added minimization command to SMT solver message
blanchet [Fri, 22 Oct 2010 11:58:33 +0200] rev 40063
bring ATPs and SMT solvers more in line with each other
blanchet [Fri, 22 Oct 2010 11:11:34 +0200] rev 40062
make Sledgehammer minimizer fully work with SMT
blanchet [Fri, 22 Oct 2010 09:50:18 +0200] rev 40061
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet [Thu, 21 Oct 2010 16:25:40 +0200] rev 40060
first step in adding support for an SMT backend to Sledgehammer
blanchet [Thu, 21 Oct 2010 14:55:09 +0200] rev 40059
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet [Thu, 21 Oct 2010 14:54:39 +0200] rev 40058
cosmetics
krauss [Fri, 22 Oct 2010 13:59:34 +0200] rev 40057
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
hoelzl [Fri, 22 Oct 2010 12:01:12 +0200] rev 40056
Changed section title to please LaTeX.
bulwahn [Thu, 21 Oct 2010 20:26:35 +0200] rev 40055
temporary removed Predicate_Compile_Quickcheck_Examples from tests
bulwahn [Thu, 21 Oct 2010 19:13:11 +0200] rev 40054
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn [Thu, 21 Oct 2010 19:13:10 +0200] rev 40053
using a signature in core_data and moving some more functions to core_data
bulwahn [Thu, 21 Oct 2010 19:13:09 +0200] rev 40052
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn [Thu, 21 Oct 2010 19:13:09 +0200] rev 40051
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn [Thu, 21 Oct 2010 19:13:08 +0200] rev 40050
for now safely but unpractically assume no predicate is terminating
bulwahn [Thu, 21 Oct 2010 19:13:07 +0200] rev 40049
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn [Thu, 21 Oct 2010 19:13:06 +0200] rev 40048
adding option smart_depth_limiting to predicate compiler
huffman [Wed, 20 Oct 2010 21:26:51 -0700] rev 40047
merged
huffman [Wed, 20 Oct 2010 19:40:02 -0700] rev 40046
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
huffman [Wed, 20 Oct 2010 17:25:22 -0700] rev 40045
add lemma lub_eq_bottom_iff
huffman [Wed, 20 Oct 2010 16:19:25 -0700] rev 40044
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman [Wed, 20 Oct 2010 13:22:30 -0700] rev 40043
constructor arguments with selectors must have pointed types
huffman [Wed, 20 Oct 2010 13:02:13 -0700] rev 40042
simplify check_and_sort_domain; more meaningful variable names
huffman [Tue, 19 Oct 2010 16:21:24 -0700] rev 40041
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman [Tue, 19 Oct 2010 15:01:51 -0700] rev 40040
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman [Tue, 19 Oct 2010 14:28:14 -0700] rev 40039
simplify some proofs; remove some unused lists of lemmas
huffman [Tue, 19 Oct 2010 11:07:42 -0700] rev 40038
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function