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.
more concise definition for Inf, Sup on bool
20110819, by haftmann
do not call ghc with fglasgowexts
20110818, by noschinl
remove some redundant simp rules about sqrt
20110819, by huffman
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
20110819, by huffman
remove unused lemma DERIV_sin_add
20110819, by huffman
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
20110819, by huffman
remove redundant lemma exp_ln_eq in favor of ln_unique
20110819, by huffman
merged
20110819, by huffman
Lim.thy: legacy theorems
20110819, by huffman
SEQ.thy: legacy theorem names
20110819, by huffman
delete unused lemmas about limits
20110819, by huffman
Transcendental.thy: add tendsto_intros lemmas;
20110819, by huffman
add lemma isCont_tendsto_compose
20110819, by huffman
merged
20110819, by wenzelm
Transcendental.thy: remove several unused lemmas and simplify some proofs
20110819, by huffman
remove unused lemmas
20110819, by huffman
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
20110819, by huffman
remove some redundant simp rules
20110819, by huffman
maintain recent future proofs at transaction boundaries;
20110819, by wenzelm
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
20110819, by wenzelm
tuned;
20110819, by wenzelm
tuned signature (again);
20110819, by wenzelm
tuned signature  treat structure Task_Queue as private to implementation;
20110819, by wenzelm
refined Future.cancel: explicit future allows to join actual cancellation;
20110819, by wenzelm
Future.promise: explicit abort operation (like uninterruptible future job);
20110819, by wenzelm
editable raw text areas: allow user to clear content;
20110819, by wenzelm
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
20110819, by wenzelm
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
20110819, by wenzelm
clarified Future.cond_forks: more uniform handling of exceptional situations;
20110819, by wenzelm
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
20110819, by Cezary Kaliszyk
less
more

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