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.
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
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
20111221, by blanchet
less
more

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