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
2011-08-17 huffman 2011-08-17 Topology_Euclidean_Space.thy: simplify some proofs
2011-08-17 huffman 2011-08-17 add lemma metric_tendsto_imp_tendsto
2011-08-17 huffman 2011-08-17 simplify proofs of lemmas open_interval, closed_interval
2011-08-17 wenzelm 2011-08-17 identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17 wenzelm 2011-08-17 clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-08-17 wenzelm 2011-08-17 tuned signature;
2011-08-17 haftmann 2011-08-17 merged
2011-08-17 haftmann 2011-08-17 merged
2011-08-17 haftmann 2011-08-17 merged
2011-08-16 haftmann 2011-08-16 avoid Collect_def in proof
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-08-17 wenzelm 2011-08-17 improved default context for ML toplevel pretty-printing;
2011-08-17 wenzelm 2011-08-17 less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-17 wenzelm 2011-08-17 some convenience actions/shortcuts for control symbols;
2011-08-17 wenzelm 2011-08-17 export Function_Fun.fun_config for user convenience;
2011-08-17 wenzelm 2011-08-17 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-17 blanchet 2011-08-17 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-16 huffman 2011-08-16 merged
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-16 wenzelm 2011-08-16 updated keywords -- old codegen is no longer in Pure;
2011-08-16 wenzelm 2011-08-16 include HOL-Library keywords for the sake of recdef;
2011-08-16 wenzelm 2011-08-16 merged
2011-08-16 huffman 2011-08-16 Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
2011-08-16 huffman 2011-08-16 get Multivariate_Analysis/Determinants.thy compiled and working again
2011-08-16 huffman 2011-08-16 get Library/Permutations.thy compiled and working again
2011-08-16 wenzelm 2011-08-16 workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16 wenzelm 2011-08-16 more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;
2011-08-16 wenzelm 2011-08-16 tuned message;
2011-08-16 wenzelm 2011-08-16 more robust treatment of node dependencies in incremental edits;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;
2011-08-16 wenzelm 2011-08-16 omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
2011-08-15 huffman 2011-08-15 merged
2011-08-15 huffman 2011-08-15 generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15 huffman 2011-08-15 add lemma tendsto_compose
2011-08-15 huffman 2011-08-15 remove extraneous subsection heading
2011-08-15 huffman 2011-08-15 generalized lemma closed_Collect_eq
2011-08-15 huffman 2011-08-15 remove duplicate lemma disjoint_iff
2011-08-15 huffman 2011-08-15 Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
2011-08-15 huffman 2011-08-15 add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;
2011-08-15 huffman 2011-08-15 generalize lemma continuous_uniform_limit to class metric_space
2011-08-15 huffman 2011-08-15 remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-15 huffman 2011-08-15 Topology_Euclidean_Space.thy: organize section headings