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.
remove some overspecific rules from the simpset
20110820, by huffman
merged
20110820, by huffman
redefine constant 'trivial_limit' as an abbreviation
20110820, by huffman
purely functional task_queue.ML  moved actual interrupt_unsynchronized to future.ML;
20110821, by wenzelm
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
20110821, by wenzelm
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
20110820, by wenzelm
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
20110820, by wenzelm
clarified get_imports  should not rely on accidental order within graph;
20110820, by wenzelm
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
20110820, by wenzelm
discontinued "Interrupt", which could disturb administrative tasks of the document model;
20110820, by wenzelm
more direct balanced version Ord_List.unions;
20110820, by wenzelm
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
20110820, by wenzelm
tuned future priorities (again);
20110820, by wenzelm
clarified fulfill_norm_proof: no join_thms yet;
20110820, by wenzelm
added Future.joins convenience;
20110820, by wenzelm
merged
20110820, by haftmann
deactivated »unknown« nitpick example
20110820, by haftmann
merged
20110820, by haftmann
tuned proof
20110820, by haftmann
more uniform formatting of specifications
20110820, by haftmann
compatibility layer
20110820, by haftmann
merged
20110820, by haftmann
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
merged
20110818, by huffman
define complex exponential 'expi' as abbreviation for 'exp'
20110818, by huffman
remove more bounded_linear locale interpretations (cf. f0de18b62d63)
20110818, by huffman
optimize some proofs
20110818, by huffman
add Multivariate_Analysis dependencies
20110818, by huffman
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
20110818, by huffman
declare euclidean_component_zero[simp] at the point it is proved
20110818, 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.
20110819, by Cezary Kaliszyk
less
more

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