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.
add rule for minus 1 at type bit
20090219, by huffman
add formalization of a type of integers mod 2 to Library
20090219, by huffman
new theory of real inner product spaces
20090219, by huffman
add Powerdomain_ex.thy
20090219, by huffman
add more ordering lemmas
20090219, by huffman
avoid using ab_semigroup_idem_mult locale for powerdomains
20090219, by huffman
merged
20090219, by huffman
add header
20090218, by huffman
move Polynomial.thy to Library
20090218, by huffman
move FrechetDeriv.thy to Library
20090218, by huffman
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
20090218, by huffman
half auto_solve default time out; increase manually in PG for large projects
20090219, by kleing
merged
20090218, by huffman
finish converting Deriv.thy to new polynomial library
20090218, by huffman
generalize int_dvd_cancel_factor simproc to idom class
20090218, by huffman
composition of polynomials
20090218, by huffman
add some lemmas, cleaned up
20090218, by huffman
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
20090218, by huffman
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
20090218, by huffman
merged
20090218, by huffman
more subsection headings
20090218, by huffman
speed up proof of exp_exists
20090218, by huffman
tuned
20090218, by haftmann
sort instances wrt. to class hierarchy
20090218, by haftmann
fixed signature
20090218, by haftmann
tuned accessor name
20090218, by haftmann
more precise improvement in instantiation user space type system
20090218, by haftmann
do not drop arguments to 0, 1
20090218, by haftmann
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
less
more

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