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.
tuned;
20120330, by wenzelm
dropped empty files
20120330, by haftmann
dropped now obsolete Cset theories
20120330, by haftmann
merged
20120330, by wenzelm
tuned proofs, less guesswork;
20120330, by wenzelm
merged
20120330, by huffman
load Tools/numeral.ML in Num.thy
20120330, by huffman
tuned proof
20120330, by huffman
set up numeral reorient simproc in Num.thy
20120330, by huffman
remove redundant simp rule
20120330, by huffman
add simp rules for eve/odd on numerals
20120330, by huffman
remove contentfree theory ex/Arithmetic_Series_Complex.thy
20120330, by huffman
rephrase lemmas about arithmetic series using numeral '2'
20120330, by huffman
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
20120330, by huffman
replace lemmas eval_nat_numeral with a simpler reformulation
20120330, by huffman
restate various simp rules for word operations using pred_numeral
20120330, by huffman
new lemmas for simplifying subtraction on nat numerals
20120330, by huffman
removed redundant natspecific copies of theorems
20120330, by huffman
move more theorems from Nat_Numeral.thy to Num.thy
20120330, by huffman
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
20120330, by wenzelm
more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);
20120330, by wenzelm
more explicit isatest environment settings (from private .bashrc);
20120330, by wenzelm
merged
20120330, by huffman
fix searchandreplace errors
20120330, by huffman
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
20120330, by huffman
add constant pred_numeral k = numeral k  (1::nat);
20120330, by huffman
move lemmas from Nat_Numeral.thy to Nat.thy
20120330, by huffman
move lemmas from Nat_Numeral to Int.thy and Num.thy
20120330, by huffman
merged
20120330, by bulwahn
adding theory to prove completeness of the exhaustive generators
20120330, by bulwahn
less
more

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