Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+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.
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
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip