Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
merged
20101022, by blanchet
compile
20101022, by blanchet
added SMT solver to Sledgehammer docs
20101022, by blanchet
more robust handling of "remote_" vs. non"remote_" provers
20101022, by blanchet
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
20101022, by blanchet
replaced references with proper record that's threaded through
20101022, by blanchet
fixed signature of "is_smt_solver_installed";
20101022, by blanchet
renamed modules
20101022, by blanchet
renamed files
20101022, by blanchet
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
20101022, by blanchet
remove more needless code ("run_smt_solvers");
20101022, by blanchet
got rid of duplicate functionality ("run_smt_solver_somehow");
20101022, by blanchet
bring ATPs and SMT solvers more in line with each other
20101022, by blanchet
make Sledgehammer minimizer fully work with SMT
20101022, by blanchet
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
20101022, by blanchet
first step in adding support for an SMT backend to Sledgehammer
20101021, by blanchet
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
20101021, by blanchet
cosmetics
20101021, by blanchet
relation method: recheck given term with type constraints to avoid unspecific failure if illtyped  keep old behaviour for tactic version
20101022, by krauss
Changed section title to please LaTeX.
20101022, by hoelzl
temporary removed Predicate_Compile_Quickcheck_Examples from tests
20101021, by bulwahn
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
20101021, by bulwahn
using a signature in core_data and moving some more functions to core_data
20101021, by bulwahn
splitting large core file into core_data, mode_inference and predicate_compile_proof
20101021, by bulwahn
added generator_dseq compilation for a sound depthlimited compilation with small value generators
20101021, by bulwahn
for now safely but unpractically assume no predicate is terminating
20101021, by bulwahn
adding decreasing bind and nondecreasing bind; depthlimited and depthunlimited compilation possible
20101021, by bulwahn
adding option smart_depth_limiting to predicate compiler
20101021, by bulwahn
merged
20101020, by huffman
introduce function strict :: 'a > 'b > 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
20101020, by huffman
add lemma lub_eq_bottom_iff
20101020, by huffman
combine check_and_sort_domain with main function; rewrite much of the errorchecking code
20101020, by huffman
constructor arguments with selectors must have pointed types
20101020, by huffman
simplify check_and_sort_domain; more meaningful variable names
20101020, by huffman
replace fixrec 'permissive' mode with perequation 'unchecked' option
20101019, by huffman
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
20101019, by huffman
simplify some proofs; remove some unused lists of lemmas
20101019, by huffman
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
20101019, by huffman
eliminate constant 'coerce'; use 'prj oo emb' instead
20101019, by huffman
simplify fixrec pattern match function
20101019, by huffman
simplify some proofs
20101017, by huffman
tuned
20101019, by Christian Urban
added some facts about factorial and dvd, div and mod
20101019, by bulwahn
removing something that probably slipped into the Quotient_List theory
20101019, by bulwahn
Quotient package: partial equivalence introduction
20101019, by Cezary Kaliszyk
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
20101018, by Christian Urban
remove dead code
20101016, by huffman
remove old uses of 'simp_tac HOLCF_ss'
20101016, by huffman
merged
20101016, by huffman
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
20101016, by huffman
reimplement proof automation for coinduct rules
20101016, by huffman
add functions mk_imp, mk_all
20101016, by huffman
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
20101015, by huffman
simplify automation of induct proof
20101015, by huffman
add function mk_adm
20101015, by huffman
rewrite proof automation for finite_ind; get rid of case_UU_tac
20101015, by huffman
put constructor argument specs in constr_info type
20101014, by huffman
avoid using Global_Theory.get_thm
20101014, by huffman
include iso_info as part of constr_info type
20101014, by huffman
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
20101014, by huffman
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip