Mercurial
Mercurial
>
repos
>
testboard
/ 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.
removed unnecessary lemmas
20120102, by nipkow
tuned proofs
20120102, by nipkow
tuned var names
20120101, by nipkow
tuned argument order
20120101, by nipkow
merged
20120101, by huffman
add simp rules for bitwise word operations with 1
20111230, by huffman
tuned types
20111231, by nipkow
disabled failing sledgehammer unit test (collateral damage of 184d36538e51)
20111231, by krauss
disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)
20111231, by krauss
merged
20111230, by berghofe
Made gen_dest_case more robust against eta contraction
20111230, by berghofe
merged
20111230, by wenzelm
remove unnecessary intermediate lemmas
20111230, by huffman
tuned;
20111230, by wenzelm
eliminated oldfashioned Global_Theory.add_thms;
20111230, by wenzelm
simplified proof  avoid res_inst_tac, afford plain asm_full_simp_tac;
20111230, by wenzelm
simplified proof;
20111230, by wenzelm
simplified proof;
20111230, by wenzelm
simplified proof;
20111230, by wenzelm
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
less
more

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