Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
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.
reduced to a compatibility layer
20111224, by haftmann
added setup for executable code
20111224, by haftmann
moved `sublists` to theory Enum
20111224, by haftmann
commented out examples which choke on strict set/pred distinction
20111224, by haftmann
explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`
20111224, by haftmann
adjusted to set/pred distinction by means of type constructor `set`
20111224, by haftmann
dropped references to obsolete fact `mem_def`
20111224, by haftmann
dropped obsolete lemma member_set
20111224, by haftmann
dropped obsolete code equation for Id
20111224, by haftmann
tuned proofs
20111224, by haftmann
generalized type signature to permit overloading on `set`
20111224, by haftmann
added monad instance for `set`
20111224, by haftmann
enum type class instance for `set`; dropped misfitting code lemma for trancl
20111224, by haftmann
finite type class instance for `set`
20111224, by haftmann
treatment of type constructor `set`
20111224, by haftmann
lattice type class instances for `set`; added code lemma for Set.bind
20111224, by haftmann
`set` is now a proper type constructor; added operation for set monad
20111224, by haftmann
simplify some proofs
20111223, by huffman
remove redundant lemma word_sub_def
20111223, by huffman
add lemmas bin_cat_zero and bin_split_zero
20111223, by huffman
more uses of 'induct arbitrary'
20111223, by huffman
use 'induct arbitrary' instead of universal quantifiers
20111223, by huffman
remove two conflicting simp rules for 'number_of (number_of _)' pattern
20111223, by huffman
add lemma bin_nth_minus1
20111222, by huffman
removed killed encoding from example
20111221, by blanchet
updated docs
20111221, by blanchet
killed "guard@?" encodings  they were found to be unsound
20111221, by blanchet
extend previous optimizations to guardbased encodings
20111221, by blanchet
treat polymorphic constructors specially in @? encodings
20111221, by blanchet
tuning
20111221, by blanchet
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
tip