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
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.
print case syntax depending on "show_cases" configuration option;
20111228, by wenzelm
merged
20111227, by huffman
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
20111227, by huffman
remove some uses of Int.succ and Int.pred
20111227, by huffman
removed unused lemmas
20111227, by huffman
remove redundant syntax declaration
20111227, by huffman
use 'induct arbitrary' instead of 'rule_format' attribute
20111227, by huffman
declare simp rules immediately, instead of using 'declare' commands
20111227, by huffman
declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin
20111227, by huffman
be explicit about Finite_Set.fold
20111227, by haftmann
dropped fact whose names clash with corresponding facts on canonical fold
20111227, by haftmann
prefer canonical fold on lists
20111227, by haftmann
be explicit about Finite_Set.fold
20111227, by haftmann
incorporated More_Set and More_List into the Main body  to be consolidated later
20111226, by haftmann
moved theorem requiring multisets from More_List to Multiset
20111226, by haftmann
NEWS: unavoidable fact renames
20111226, by haftmann
dropped disfruitful `constant signatures`
20111226, by haftmann
moved various set operations to theory Set (resp. Product_Type)
20111226, by haftmann
dropped Executable_Set wrapper theory
20111226, by haftmann
updated certificate
20111225, by haftmann
NEWS: `set` is now a proper type constructor
20111224, by haftmann
dropped references to obsolete facts `mem_def` and `Collect_def`
20111224, by haftmann
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
20111224, by haftmann
adjusted to set/pred distinction by means of type constructor `set`
20111224, by haftmann
treatment of type constructor `set`
20111224, by haftmann
executable intervals
20111224, by haftmann
`set` is now a proper type constructor
20111224, by haftmann
tuned layout
20111224, by haftmann
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
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
20111221, by blanchet
added some basic documentation about method induction_schema extracted from old NEWS
20111221, by bulwahn
less
more

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