2011-08-19 huffman 2011-08-19 delete unused lemmas about limits
2011-08-19 huffman 2011-08-19 Transcendental.thy: add tendsto_intros lemmas; new isCont theorems; simplify some proofs.
2011-08-19 huffman 2011-08-19 add lemma isCont_tendsto_compose
2011-08-19 wenzelm 2011-08-19 merged
2011-08-19 huffman 2011-08-19 Transcendental.thy: remove several unused lemmas and simplify some proofs
2011-08-19 huffman 2011-08-19 remove unused lemmas
2011-08-19 huffman 2011-08-19 fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2011-08-19 huffman 2011-08-19 remove some redundant simp rules
2011-08-19 wenzelm 2011-08-19 maintain recent future proofs at transaction boundaries;
2011-08-19 wenzelm 2011-08-19 incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature (again); tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19 wenzelm 2011-08-19 refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;
2011-08-19 wenzelm 2011-08-19 Future.promise: explicit abort operation (like uninterruptible future job); explicit cancel_scala message -- still unused;
2011-08-19 wenzelm 2011-08-19 editable raw text areas: allow user to clear content;
2011-08-19 wenzelm 2011-08-19 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
2011-08-19 wenzelm 2011-08-19 more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-19 wenzelm 2011-08-19 clarified Future.cond_forks: more uniform handling of exceptional situations;
2011-08-19 Cezary Kaliszyk 2011-08-19 Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
2011-08-18 huffman 2011-08-18 merged
2011-08-18 huffman 2011-08-18 define complex exponential 'expi' as abbreviation for 'exp'
2011-08-18 huffman 2011-08-18 remove more bounded_linear locale interpretations (cf. f0de18b62d63)
2011-08-18 huffman 2011-08-18 optimize some proofs
2011-08-18 huffman 2011-08-18 add Multivariate_Analysis dependencies
2011-08-18 huffman 2011-08-18 import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
2011-08-18 huffman 2011-08-18 declare euclidean_component_zero[simp] at the point it is proved
2011-08-19 Cezary Kaliszyk 2011-08-19 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-18 wenzelm 2011-08-18 merged;
2011-08-18 huffman 2011-08-18 merged
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-18 haftmann 2011-08-18 merged
2011-08-18 haftmann 2011-08-18 merged
2011-08-18 haftmann 2011-08-18 avoid duplicated simp add option
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-08-18 haftmann 2011-08-18 moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-18 haftmann 2011-08-18 avoid case-sensitive name for example theory
2011-08-18 nipkow 2011-08-18 merged
2011-08-18 nipkow 2011-08-18 case_names NEWS
2011-08-18 bulwahn 2011-08-18 adding documentation about simps equation in the inductive package
2011-08-18 bulwahn 2011-08-18 activating narrowing-based quickcheck by default
2011-08-18 wenzelm 2011-08-18 more precise treatment of exception nesting and serial numbers;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18 wenzelm 2011-08-18 updated sequential version (cf. b94951f06e48);
2011-08-18 wenzelm 2011-08-18 tuned comments;
2011-08-18 wenzelm 2011-08-18 tuned document; tuned proofs;
2011-08-18 wenzelm 2011-08-18 clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
2011-08-18 wenzelm 2011-08-18 export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
2011-08-18 wenzelm 2011-08-18 tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;
2011-08-18 Cezary Kaliszyk 2011-08-18 Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
2011-08-17 huffman 2011-08-17 merged
2011-08-17 huffman 2011-08-17 HOL-IMP: respect set/pred distinction
2011-08-17 huffman 2011-08-17 Determinants.thy: avoid using mem_def/Collect_def
2011-08-17 huffman 2011-08-17 Wfrec.thy: respect set/pred distinction
2011-08-18 wenzelm 2011-08-18 follow updates of Isabelle/Pure;
2011-08-17 wenzelm 2011-08-17 merged
2011-08-17 huffman 2011-08-17 IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
2011-08-17 huffman 2011-08-17 merged
2011-08-17 huffman 2011-08-17 Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
2011-08-17 huffman 2011-08-17 add lemma tendsto_compose_eventually; use it to shorten some proofs