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 precise Local_Defs.expand wrt. *local* prems only;
20120331, by wenzelm
tuned comment;
20120331, by wenzelm
more robust Scala 2.9.x interpreter invocation  avoid separate interpreter thread and thus deadlock of Swing_Thread.now;
20120330, by wenzelm
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
refine bindings in quickcheck_common: do not conceal and do not declare as simps
20120330, by bulwahn
hiding fact not so aggressively
20120330, by bulwahn
power on predicate relations
20120330, by haftmann
made MirabelleSH's 'trivial' check optional;
20120330, by sultana
merged
20120329, by wenzelm
more specific notion of partiality (cf. Scala version);
20120329, by wenzelm
use qualified names for rsp and rep_eq theorems in quotient_def
20120329, by kuncar
announcing NEWS (cf. 446cfc760ccf)
20120329, by bulwahn
remove obsolete simp rule for powers
20120329, by huffman
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
20120329, by huffman
remove unneeded rewrite rules for powers of numerals
20120329, by huffman
remove duplicate lemma Suc_numeral
20120329, by huffman
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
20120329, by huffman
bootstrap Num.thy before Power.thy;
20120329, by huffman
educated guess to include jdk
20120329, by haftmann
improved robustness with new antiquoation by Makarius
20120328, by nipkow
merged
20120328, by nipkow
updates
20120328, by nipkow
updated documentation files (cf. c14fda8fee38)
20120328, by bulwahn
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
20120328, by wenzelm
merged
20120328, by wenzelm
removed references to obsolete theorems
20120328, by huffman
merged
20120328, by bulwahn
some tuning while reviewing the current state of the quotient_def package
20120328, by bulwahn
improving spelling
20120328, by bulwahn
changing more definitions to quotient_definition
20120328, by bulwahn
removing now redundant impl_of theorems in DAList
20120328, by bulwahn
less
more

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