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
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
deactivated »unknown« nitpick example
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
tuned proof
2011-08-20, by haftmann
more uniform formatting of specifications
2011-08-20, by haftmann
compatibility layer
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
more concise definition for Inf, Sup on bool
2011-08-19, by haftmann
do not call ghc with -fglasgow-exts
2011-08-18, by noschinl
remove some redundant simp rules about sqrt
2011-08-19, by huffman
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-19, by huffman
remove unused lemma DERIV_sin_add
2011-08-19, by huffman
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19, by huffman
remove redundant lemma exp_ln_eq in favor of ln_unique
2011-08-19, by huffman
merged
2011-08-19, by huffman
Lim.thy: legacy theorems
2011-08-19, by huffman
SEQ.thy: legacy theorem names
2011-08-19, by huffman
delete unused lemmas about limits
2011-08-19, by huffman
Transcendental.thy: add tendsto_intros lemmas;
2011-08-19, by huffman
add lemma isCont_tendsto_compose
2011-08-19, by huffman
merged
2011-08-19, by wenzelm
Transcendental.thy: remove several unused lemmas and simplify some proofs
2011-08-19, by huffman
remove unused lemmas
2011-08-19, by huffman
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2011-08-19, by huffman
remove some redundant simp rules
2011-08-19, by huffman
maintain recent future proofs at transaction boundaries;
2011-08-19, by wenzelm
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19, by wenzelm
tuned;
2011-08-19, by wenzelm
tuned signature (again);
2011-08-19, by wenzelm
tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19, by wenzelm
refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-19, by wenzelm
Future.promise: explicit abort operation (like uninterruptible future job);
2011-08-19, by wenzelm
editable raw text areas: allow user to clear content;
2011-08-19, by wenzelm
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
2011-08-19, by wenzelm
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-19, by wenzelm
clarified Future.cond_forks: more uniform handling of exceptional situations;
2011-08-19, by wenzelm
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
2011-08-19, by Cezary Kaliszyk
merged
2011-08-18, by huffman
define complex exponential 'expi' as abbreviation for 'exp'
2011-08-18, by huffman
remove more bounded_linear locale interpretations (cf. f0de18b62d63)
2011-08-18, by huffman
optimize some proofs
2011-08-18, by huffman
add Multivariate_Analysis dependencies
2011-08-18, by huffman
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
2011-08-18, by huffman
declare euclidean_component_zero[simp] at the point it is proved
2011-08-18, by huffman
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
2011-08-19, by Cezary Kaliszyk
merged;
2011-08-18, by wenzelm
merged
2011-08-18, by huffman
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-18, by huffman
merged
2011-08-18, by haftmann
merged
2011-08-18, by haftmann
avoid duplicated simp add option
2011-08-18, by haftmann
observe distinction between sets and predicates more properly
2011-08-18, by haftmann
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-18, by haftmann
avoid case-sensitive name for example theory
2011-08-18, by haftmann
merged
2011-08-18, by nipkow
case_names NEWS
2011-08-18, by nipkow
adding documentation about simps equation in the inductive package
2011-08-18, by bulwahn
activating narrowing-based quickcheck by default
2011-08-18, by bulwahn
more precise treatment of exception nesting and serial numbers;
2011-08-18, by wenzelm
more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18, by wenzelm
updated sequential version (cf. b94951f06e48);
2011-08-18, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip