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 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
using abstract code equations for proofs of code equations in Multiset
20120328, by bulwahn
simplified statements and proofs;
20120328, by wenzelm
tuned whitespace;
20120328, by wenzelm
updated Sign.add_type, Name_Space.declare;
20120328, by wenzelm
updated comments;
20120328, by wenzelm
merged
20120328, by huffman
remove unnecessary rules from the simpset
20120327, by huffman
remove unused premises
20120327, by huffman
remove duplicate lemmas
20120327, by huffman
mark some duplicate lemmas for deletion
20120327, by huffman
remove more redundant lemmas
20120327, by huffman
tuned proofs
20120327, by huffman
remove redundant lemmas
20120327, by huffman
generalized lemma zpower_zmod
20120327, by huffman
remove redundant lemma
20120327, by huffman
remove redundant lemma
20120327, by huffman
remove duplicate [algebra] declarations
20120327, by huffman
generalize more div/mod lemmas
20120327, by huffman
generalize some theorems about div/mod
20120327, by huffman
updated to jedit4.5.1;
20120328, by wenzelm
merged
20120327, by kuncar
note a code eqn in quotient_def
20120327, by kuncar
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
20120327, by boehmes
less
more

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