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.
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
merged;
20110818, by wenzelm
merged
20110818, by huffman
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
20110818, by huffman
merged
20110818, by haftmann
merged
20110818, by haftmann
avoid duplicated simp add option
20110818, by haftmann
observe distinction between sets and predicates more properly
20110818, by haftmann
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
20110818, by haftmann
avoid casesensitive name for example theory
20110818, by haftmann
merged
20110818, by nipkow
case_names NEWS
20110818, by nipkow
adding documentation about simps equation in the inductive package
20110818, by bulwahn
activating narrowingbased quickcheck by default
20110818, by bulwahn
more precise treatment of exception nesting and serial numbers;
20110818, by wenzelm
more careful treatment of exception serial numbers, with propagation to message channel;
20110818, by wenzelm
updated sequential version (cf. b94951f06e48);
20110818, by wenzelm
tuned comments;
20110818, by wenzelm
tuned document;
20110818, by wenzelm
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
20110818, by wenzelm
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
20110818, by wenzelm
tune Par_Exn.make: balance merge;
20110818, by wenzelm
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
20110818, by Cezary Kaliszyk
merged
20110817, by huffman
HOLIMP: respect set/pred distinction
20110817, by huffman
Determinants.thy: avoid using mem_def/Collect_def
20110817, by huffman
Wfrec.thy: respect set/pred distinction
20110817, by huffman
follow updates of Isabelle/Pure;
20110818, by wenzelm
merged
20110817, by wenzelm
IsaMakefile: target HOLCFLibrary now compiles HOL/HOLCF/Library instead of HOL/Library
20110817, by huffman
merged
20110817, by huffman
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
20110817, by huffman
add lemma tendsto_compose_eventually; use it to shorten some proofs
20110817, by huffman
Topology_Euclidean_Space.thy: simplify some proofs
20110817, by huffman
add lemma metric_tendsto_imp_tendsto
20110817, by huffman
simplify proofs of lemmas open_interval, closed_interval
20110817, by huffman
identify parallel exceptions where they emerge first  to achieve unique results within evaluation graph;
20110817, by wenzelm
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
20110817, by wenzelm
more systematic handling of parallel exceptions;
20110817, by wenzelm
tuned signature;
20110817, by wenzelm
merged
20110817, by haftmann
less
more

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