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.
more parallelism;
20111230, by wenzelm
tuned;
20111230, by wenzelm
merged
20111229, by wenzelm
tuned  afford slightly larger simpset in simp_defs_tac;
20111229, by wenzelm
tuned  standard proofs by default;
20111229, by wenzelm
do not fork skipped proofs;
20111229, by wenzelm
clarified timeit_msg;
20111229, by wenzelm
tuned;
20111229, by wenzelm
comments;
20111229, by wenzelm
remove constant 'ccpo.lub', reuse constant 'Sup' instead
20111229, by huffman
merged
20111229, by nipkow
tuned
20111229, by nipkow
conversions from sets to predicates and vice versa; extensionality on predicates
20111229, by haftmann
added implementation of pred_of_set
20111229, by haftmann
fundamental theorems on Set.bind
20111229, by haftmann
updated generated files;
20111229, by wenzelm
qualified Finite_Set.fold
20111229, by haftmann
qualified Finite_Set.fold
20111229, by haftmann
dropped redundant setup
20111229, by haftmann
tuned declaration
20111229, by haftmann
attribute code_abbrev superseedes code_unfold_post; tuned text
20111229, by haftmann
attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
20111229, by haftmann
attribute code_abbrev superseedes code_unfold_post
20111229, by haftmann
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
20111229, by haftmann
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
20111229, by haftmann
merged
20111228, by wenzelm
merged
20111228, by huffman
restate some lemmas to respect int/bin distinction
20111228, by huffman
simplify some proofs
20111228, by huffman
add lemma word_eq_iff
20111228, by huffman
restate lemma word_1_no in terms of Numeral1
20111228, by huffman
remove recursion combinator bin_rec;
20111228, by huffman
simplify definition of XOR for type int;
20111228, by huffman
simplify definition of OR for type int;
20111228, by huffman
simplify definition of NOT for type int
20111228, by huffman
add several new tests, most of which don't work yet
20111228, by huffman
fix typos
20111228, by huffman
remove some duplicate lemmas
20111228, by huffman
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
less
more

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