Mercurial
Mercurial
>
repos
>
testboard
/ 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.
removed redundant thms
20090221, by nipkow
merged
20090220, by huffman
class instances for num1
20090220, by huffman
Removed redundant lemmas
20090220, by nipkow
merged
20090220, by haftmann
also consider superclasses properly
20090220, by haftmann
merged
20090220, by nipkow
removed subsumed lemmas
20090220, by nipkow
merged
20090220, by haftmann
datatype antiquotation: always bracket types with spaces in between
20090220, by haftmann
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
less
more

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