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
+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
less
more

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