2011-08-13 ago wenzelm simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13 ago wenzelm simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 ago wenzelm provide node header via Scala layer;
2011-08-13 ago wenzelm reduced verbosity;
2011-08-13 ago wenzelm tuned signature;
2011-08-13 ago wenzelm clarified node header -- exclude master_dir;
2011-08-13 ago wenzelm tuned;
2011-08-13 ago wenzelm maintain node header;
2011-08-13 ago kleing removed unused lemma; removed old-style ;
2011-08-13 ago kleing point isatest-statistics to the right afp log files
2011-08-13 ago kleing IMP/Util distinguishes between sets and functions again; imported only where used.
2011-08-12 ago huffman remove redundant lemma setsum_norm in favor of norm_setsum;
2011-08-12 ago huffman merged
2011-08-12 ago huffman make more HOL theories work with separate set type
2011-08-13 ago wenzelm immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
2011-08-12 ago wenzelm merged
2011-08-12 ago huffman merged
2011-08-12 ago huffman make Multivariate_Analysis work with separate set type
2011-08-12 ago huffman make HOLCF work with separate set type
2011-08-12 ago huffman merged
2011-08-11 ago huffman avoid duplicate rule warnings
2011-08-11 ago huffman modify euclidean_space class to include basis set
2011-08-11 ago huffman remove lemma stupid_ext
2011-08-12 ago nipkow documented extended version of case_names attribute
2011-08-12 ago wenzelm normalized theory dependencies wrt. file_store;
2011-08-12 ago wenzelm general Graph.schedule;
2011-08-12 ago wenzelm allow "$" within basic path elements (NB: initial "$" refers to path variable);
2011-08-12 ago wenzelm clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-12 ago wenzelm simplified class Thy_Header;
2011-08-12 ago wenzelm clarified Exn.message;
2011-08-11 ago wenzelm uniform treatment of header edits as document edits;
2011-08-11 ago wenzelm explicit datatypes for document node edits;
2011-08-11 ago wenzelm tuned;
2011-08-11 ago wenzelm disentangled nested ML files;
2011-08-11 ago wenzelm minimal script to run raw Poly/ML with concurrency library;
2011-08-11 ago wenzelm somewhat more uniform THIS;
2011-08-11 ago wenzelm more trimming;
2011-08-11 ago wenzelm recovered some ML toplevel pp;
2011-08-11 ago wenzelm some trimming;
2011-08-11 ago wenzelm prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
2011-08-11 ago wenzelm redundant use of misc_legacy.ML;
2011-08-11 ago krauss eliminated use of recdef
2011-08-11 ago krauss removed obsolete recdef-related examples
2011-08-11 ago krauss removed unused material, which does not really belong here
2011-08-10 ago huffman merged
2011-08-10 ago huffman avoid warnings about duplicate rules
2011-08-10 ago huffman follow standard naming scheme for sgn_vec_def
2011-08-10 ago huffman remove several redundant and unused theorems about derivatives
2011-08-10 ago huffman remove redundant lemma
2011-08-10 ago huffman simplify proof of lemma bounded_component
2011-08-10 ago huffman simplify some proofs
2011-08-10 ago huffman more uniform naming scheme for finite cartesian product type and related theorems
2011-08-10 ago huffman move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
2011-08-10 ago wenzelm merged
2011-08-10 ago huffman split Linear_Algebra.thy from Euclidean_Space.thy
2011-08-10 ago huffman full import paths
2011-08-10 ago huffman declare tendsto_const [intro] (accidentally removed in 230a8665c919)
2011-08-10 ago huffman merged
2011-08-10 ago huffman simplified definition of class euclidean_space;
2011-08-09 ago huffman bounded_linear interpretation for euclidean_component