Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
120
+120
+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.
consequent use of term `code equation`
20090220, by haftmann
permissive check for pattern discipline in case schemes
20090220, by haftmann
maintain order of constructors in datatypes; clarified conventions for type schemes
20090220, by haftmann
stripped Id
20090220, by haftmann
merged
20090220, by huffman
add theory of products as real vector spaces to Library
20090220, by huffman
add new theory Product_plus.thy to Library
20090220, by huffman
merged
20090220, by immler
changed message
20090220, by immler
detailed information on atpfailure via Output.debug
20090220, by immler
merged
20090220, by haftmann
reverted to old wellsorting algorithm
20090220, by haftmann
fixed spurious proof failure
20090220, by haftmann
consider changes variable names in theorem le_imp_power_dvd
20090220, by haftmann
tuned and incremental version of wellsorting algorithm
20090220, by haftmann
ignore sorts in bare types
20090220, by haftmann
defensive implementation of pretty serialisation of lists and characters
20090220, by haftmann
dropped Id
20090220, by haftmann
experimental inclusion of new wellsorting algorithm for code equations
20090220, by haftmann
merged
20090220, by chaieb
merged
20090217, by chaieb
merged
20090217, by chaieb
fixed selection of premises
20090217, by chaieb
cleaned up
20090219, by huffman
declare of_int_number_of_eq [simp]
20090219, by huffman
fix case_names
20090219, by huffman
nicer induction/cases rules for numeral types
20090219, by huffman
number_ring instances for numeral types
20090219, by huffman
declare xor_compl_{left,right} [simp]
20090219, by huffman
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
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
less
more

(0)
30000
10000
3000
1000
120
+120
+1000
+3000
+10000
+30000
tip