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.
merged
20090218, by haftmann
reverted to previous version of Finite_Set.thy
20090218, by haftmann
merged
20090218, by haftmann
merged
20090218, by haftmann
first working version
20090218, by haftmann
tuned comments, stripped ID, deleted superfluous code
20090218, by haftmann
stripped ID
20090218, by haftmann
Syntactic support for products over set intervals
20090218, by paulson
No idea what happened here!
20090218, by paulson
Even and odd powers of 1
20090217, by paulson
merged
20090218, by blanchet
Reintroduce set_interpreter for Collect and op :.
20090217, by blanchet
Added Nitpick tag to 'of_int_of_nat'.
20090216, by blanchet
add lemmas for exponentiation
20090217, by huffman
merged
20090217, by haftmann
unified variable names in case expressions; no exponential fork in translation of case expressions
20090217, by haftmann
merged
20090217, by huffman
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
less
more

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