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
2011-08-15 huffman 2011-08-15 simplify some proofs
2011-08-14 huffman 2011-08-14 generalize lemma convergent_subseq_convergent
2011-08-14 huffman 2011-08-14 locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
2011-08-14 huffman 2011-08-14 locale-ize some constant definitions, so complete_space can inherit from metric_space
2011-08-14 huffman 2011-08-14 generalize constant 'lim' and limit uniqueness theorems to class t2_space
2011-08-16 Cezary Kaliszyk 2011-08-16 Quotient Package: make quotient_type work with separate set type
2011-08-15 wenzelm 2011-08-15 updated README;
2011-08-15 wenzelm 2011-08-15 touch descendants of edited nodes; more precise handling of Graph exceptions;
2011-08-15 wenzelm 2011-08-15 parellel scheduling of node edits and execution;
2011-08-15 wenzelm 2011-08-15 tuned error message;
2011-08-15 wenzelm 2011-08-15 retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;
2011-08-15 wenzelm 2011-08-15 explicit check of finished evaluation;
2011-08-15 wenzelm 2011-08-15 refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;
2011-08-15 wenzelm 2011-08-15 simplified exec: eliminated unused status flag;
2011-08-14 huffman 2011-08-14 consistently use variable name 'F' for filters
2011-08-14 huffman 2011-08-14 generalize lemmas about LIM and LIMSEQ to tendsto
2011-08-13 huffman 2011-08-13 HOL-Nominal-Examples: respect distinction between sets and functions
2011-08-13 wenzelm 2011-08-13 less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;
2011-08-13 wenzelm 2011-08-13 merged
2011-08-13 huffman 2011-08-13 HOL-Hahn_Banach: use Set_Algebras library
2011-08-13 huffman 2011-08-13 ex/Quickcheck_Examples.thy: respect distinction between sets and functions
2011-08-13 wenzelm 2011-08-13 clarified Toplevel.end_theory;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-13 wenzelm 2011-08-13 reduced verbosity;
2011-08-13 wenzelm 2011-08-13 tuned signature;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-13 wenzelm 2011-08-13 tuned;
2011-08-13 wenzelm 2011-08-13 maintain node header; misc tuning and clarification;
2011-08-13 kleing 2011-08-13 removed unused lemma; removed old-style ;
2011-08-13 kleing 2011-08-13 point isatest-statistics to the right afp log files