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.
merged
20090222, by nipkow
name fix
20090222, by nipkow
fix spelling
20090221, by huffman
real_inner class instance for vectors
20090221, by huffman
NEWS
20090221, by nipkow
merged
20090221, by nipkow
Removed subsumed lemmas
20090221, by nipkow
remove duplicated lemmas about norm
20090221, by huffman
real_normed_vector instance
20090221, by huffman
fix real_vector, real_algebra instances
20090221, by huffman
merged
20090221, by huffman
generalize lemmas from nat to 'a::wellorder
20090220, by huffman
generalize some lemmas
20090220, by huffman
merged
20090221, by nipkow
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
less
more

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