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
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.
example cleanup
20111118, by blanchet
example cleanup
20111118, by blanchet
don't propagate userset "type_enc" or "lam_trans" to Metis calls
20111118, by blanchet
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
20111118, by blanchet
avoid spurious messages in "lam_lifting" mode
20111118, by blanchet
etacontract to avoid needless "lambda" wrappers
20111118, by blanchet
quiet down SMT
20111118, by blanchet
more aggressive lambda hiding (if we anyway need to pass an option to Metis)
20111118, by blanchet
updated Sledgehammer docs
20111118, by blanchet
don't pass "lam_lifted" option to "metis" unless there's a good reason
20111118, by blanchet
no needless reconstructors
20111118, by blanchet
removed more clutter
20111118, by blanchet
removed needless baggage
20111118, by blanchet
Word.thy: reduce usage of numeralrepresentationdependent thms like number_of_is_id in proofs
20111118, by huffman
merged
20111118, by huffman
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
20111117, by huffman
HOLWord: removed more duplicate theorems
20111117, by huffman
HOLWord: removed many duplicate theorems (see NEWS)
20111117, by huffman
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
20111117, by huffman
move definitions of bitwise operators into appropriate document section
20111117, by huffman
HOLWord: add simp rules for bin_rest, bin_last; shorten several proofs
20111117, by huffman
HOLNSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
20111117, by huffman
simplify implementation of approx_reorient_simproc
20111117, by huffman
name simp theorems st_0 and st_1
20111117, by huffman
remove redundant simp rules plus_enat_0
20111117, by huffman
eliminated slightly odd Rep' with dynamicallyscoped [simplified];
20111117, by wenzelm
partial evaluation in invisible context;
20111117, by wenzelm
adding a preliminary example to show how the quotient_definition package can be generalized
20111117, by bulwahn
tuned header
20111117, by bulwahn
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
20111117, by bulwahn
simplify some proofs
20111117, by huffman
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
20111117, by huffman
merged
20111117, by huffman
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
20111116, by huffman
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
20111116, by huffman
simplify proof of word_of_int; remove several nowunused lemmas about Rep_Integ
20111116, by huffman
retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
20111116, by wenzelm
clarified Attrib.partial_evaluation;
20111116, by wenzelm
tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
20111116, by wenzelm
compile
20111116, by blanchet
compile
20111116, by blanchet
compile
20111116, by blanchet
give each time slice its own lambda translation
20111116, by blanchet
thread in additional options to minimizer
20111116, by blanchet
make metis reconstruction handling more flexible
20111116, by blanchet
document metis options better
20111116, by blanchet
fixed typo
20111116, by blanchet
document "lam_trans" option
20111116, by blanchet
nicer bullets
20111116, by blanchet
parse lambda translation option in Metis
20111116, by blanchet
rename the lambda translation schemes, so that they are understandable out of context
20111115, by blanchet
rename configuration option to more reasonable length
20111115, by blanchet
continued implementation of lambdalifting in Metis
20111115, by blanchet
disable debugging output
20111115, by blanchet
use consts, not frees, for lambdalifting
20111115, by blanchet
started implementing lambdalifting in Metis
20111115, by blanchet
improved generators for rational numbers to generate negative numbers;
20111115, by bulwahn
tuned
20111115, by bulwahn
remove one more oldstyle semicolon
20111115, by huffman
Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs
20111115, by huffman
less
more

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