Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
remove redundant simp attributes for zdvd rules
20090217, by huffman
lemmas abs_dvd_iff, dvd_abs_iff
20090217, by huffman
Cleaned up IntDiv and removed subsumed lemmas.
20090217, by nipkow
tune section headings; add square function
20090216, by huffman
merged
20090216, by huffman
rearrange subsections
20090216, by huffman
remove instances num::semiring and num::linorder
20090216, by huffman
datatype num = One  Dig0 num  Dig1 num
20090216, by huffman
replace 1::num with One; remove monoid_mult instance
20090216, by huffman
replace dec with doubleanddecrement function
20090215, by huffman
more default simp rules for sgn
20090216, by haftmann
regenerated
20090216, by haftmann
clarified import
20090216, by haftmann
faster preprocessor
20090216, by haftmann
added pdivmod on int (for code generation)
20090216, by haftmann
merged
20090216, by haftmann
tuned texts
20090216, by haftmann
dropped Id
20090216, by haftmann
dropped clause_suc_preproc for generic code generator
20090216, by haftmann
new primrec
20090216, by haftmann
Adapted to encoding of sets as predicates.
20090216, by berghofe
enable autosolve by default
20090216, by kleing
merged
20090216, by blanchet
Added nitpick attribute, and fixed typo.
20090216, by blanchet
Added myself to testing list.
20090216, by blanchet
dvd and setprod lemmas
20090215, by nipkow
merged
20090215, by nipkow
added finite_set_choice
20090215, by nipkow
reject defined function in patterns with errmsg, e.g. f (f x) = x
20090215, by krauss
fixed document
20090215, by nipkow
more finiteness
20090215, by nipkow
merged
20090215, by nipkow
more finiteness
20090215, by nipkow
merged
20090214, by nipkow
more finiteness
20090214, by nipkow
generalize lemma fps_square_eq_iff, move to Ring_and_Field
20090214, by huffman
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
20090214, by huffman
add mult_delta lemmas; simplify some proofs
20090214, by huffman
fix spelling
20090214, by huffman
declare fps_nth as a typedef morphism; clean up instance proofs
20090214, by huffman
add lemma surj_from_nat
20090214, by huffman
fix document generation
20090214, by huffman
merged
20090214, by huffman
fix document generation
20090214, by huffman
section > subsection
20090213, by huffman
add instance for cancel_comm_monoid_add
20090213, by huffman
add class cancel_comm_monoid_add
20090213, by huffman
more finiteness changes
20090214, by nipkow
merged
20090213, by nipkow
finiteness lemmas
20090213, by nipkow
merged
20090213, by huffman
unset execute bit
20090213, by huffman
Tuned datatype antiquotation.
20090213, by berghofe
made SMLNJ happy
20090213, by haftmann
typo
20090213, by kleing
find_consts: display the search criteria. (by Timothy Bourke)
20090213, by kleing
find_consts: documentation. (by Timothy Bourke)
20090213, by kleing
FindTheorems solves: update documentation (by Timothy Bourke)
20090213, by kleing
fixed codegen tool
20090213, by haftmann
merged
20090213, by haftmann
less
more

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