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.
simplify proof
20111228, by huffman
replace 'lemmas' with explicit 'lemma'
20111228, by huffman
add section headings
20111228, by huffman
remove duplicate lemma lists
20111227, by huffman
reverted some changes for set>predicate transition, according to "hg log u berghofe r Isabelle2007:Isabelle2008";
20111228, by wenzelm
disable kodkodi for now to prevent isatest failure of HOLNitpick_Examples due to 'a set constructor;
20111228, by wenzelm
updated platform information;
20111228, by wenzelm
discontinued broken macbroy5 and thus the obsolete ppcdarwin platform;
20111228, by wenzelm
more selective target "full"  avoid failure of HOLDatatype_Benchmark on 32bit platforms;
20111228, by wenzelm
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
less
more

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