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.
CONTRIBUTORS
20101025, by haftmann
merge
20101025, by blanchet
merged
20101025, by blanchet
updated keywords
20101025, by blanchet
introduced manual version of "Auto Solve" as "solve_direct"
20101025, by blanchet
make "sledgehammer_params" work on singlethreaded platforms
20101025, by blanchet
tuning
20101022, by blanchet
handle timeouts (to prevent failure from other threads);
20101022, by blanchet
update keywords
20101025, by haftmann
some partial_function examples
20101025, by krauss
added ML antiquotation @{assert};
20101025, by wenzelm
updated keywords;
20101025, by wenzelm
integrated partial_function into HOLPlain
20101023, by krauss
first version of partial_function package
20101023, by krauss
Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem
20101023, by krauss
merged
20101025, by bulwahn
splitting Hotel Key card example into specification and the two tests for counter example generation
20101022, by bulwahn
adding generator quickcheck
20101022, by bulwahn
restructuring values command and adding generator compilation
20101022, by bulwahn
moving general functions from core_data to predicate_compile_aux
20101022, by bulwahn
updating to new notation in commented examples
20101022, by bulwahn
merged
20101024, by huffman
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
20101024, by huffman
remove legacy comp_dbind option from domain package
20101023, by huffman
change fixrec parser to not accept theorem names with (unchecked) option
20101023, by huffman
tuned
20101023, by huffman
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
20101022, by huffman
add lemma strict3
20101022, by huffman
do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas
20101022, by huffman
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
20101022, by huffman
direct instantiation unit :: discrete_cpo
20101022, by huffman
remove finite_po class
20101022, by huffman
simplify proofs about flift; remove unneeded lemmas
20101022, by huffman
simplify proof
20101022, by huffman
minimize imports
20101021, by huffman
add type annotation to avoid warning
20101021, by huffman
simplify some proofs, convert to Isar style
20101021, by huffman
rename lemma spair_lemma to spair_Sprod
20101021, by huffman
pcpodef (open) 'a lift
20101021, by huffman
remove intro! attribute from {sinl,sinr}_defined
20101021, by huffman
simplify proofs of ssumE, sprodE
20101021, by huffman
merged
20101024, by wenzelm
renamed nat_number
20101024, by nipkow
nat_number > eval_nat_numeral
20101024, by nipkow
some cleanup in Function_Lib
20101022, by krauss
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
less
more

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