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.
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
tuned comments;
2011-08-18, by wenzelm
tuned document;
2011-08-18, by wenzelm
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
2011-08-18, by wenzelm
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
2011-08-18, by wenzelm
tune Par_Exn.make: balance merge;
2011-08-18, by wenzelm
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
2011-08-18, by Cezary Kaliszyk
merged
2011-08-17, by huffman
HOL-IMP: respect set/pred distinction
2011-08-17, by huffman
Determinants.thy: avoid using mem_def/Collect_def
2011-08-17, by huffman
Wfrec.thy: respect set/pred distinction
2011-08-17, by huffman
follow updates of Isabelle/Pure;
2011-08-18, by wenzelm
merged
2011-08-17, by wenzelm
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
2011-08-17, by huffman
merged
2011-08-17, by huffman
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
2011-08-17, by huffman
add lemma tendsto_compose_eventually; use it to shorten some proofs
2011-08-17, by huffman
Topology_Euclidean_Space.thy: simplify some proofs
2011-08-17, by huffman
add lemma metric_tendsto_imp_tendsto
2011-08-17, by huffman
simplify proofs of lemmas open_interval, closed_interval
2011-08-17, by huffman
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip