isabelle: Graph

avoid Collect_def in proof
2011-08-16, by haftmann
modernized signature of Term.absfree/absdummy;
2011-08-17, by wenzelm
improved default context for ML toplevel pretty-printing;
2011-08-17, by wenzelm
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-17, by wenzelm
some convenience actions/shortcuts for control symbols;
2011-08-17, by wenzelm
export Function_Fun.fun_config for user convenience;
2011-08-17, by wenzelm
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-17, by wenzelm
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-17, by blanchet
merged
2011-08-16, by huffman
add simp rules for isCont
2011-08-16, by huffman
updated keywords -- old codegen is no longer in Pure;
2011-08-16, by wenzelm
include HOL-Library keywords for the sake of recdef;
2011-08-16, by wenzelm
merged
2011-08-16, by wenzelm
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
2011-08-16, by huffman
get Multivariate_Analysis/Determinants.thy compiled and working again
2011-08-16, by huffman
get Library/Permutations.thy compiled and working again
2011-08-16, by huffman
workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16, by wenzelm
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
2011-08-16, by wenzelm
tuned message;
2011-08-16, by wenzelm
more robust treatment of node dependencies in incremental edits;
2011-08-16, by wenzelm
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
2011-08-16, by wenzelm
omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
2011-08-16, by wenzelm
merged
2011-08-15, by huffman
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15, by huffman
add lemma tendsto_compose
2011-08-15, by huffman
remove extraneous subsection heading
2011-08-15, by huffman
generalized lemma closed_Collect_eq
2011-08-15, by huffman
remove duplicate lemma disjoint_iff
2011-08-15, by huffman
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
2011-08-15, by huffman
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
2011-08-15, by huffman
generalize lemma continuous_uniform_limit to class metric_space
2011-08-15, by huffman
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-15, by huffman
Topology_Euclidean_Space.thy: organize section headings
2011-08-15, by huffman
simplify some proofs
2011-08-15, by huffman
generalize lemma convergent_subseq_convergent
2011-08-14, by huffman
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
2011-08-14, by huffman
locale-ize some constant definitions, so complete_space can inherit from metric_space
2011-08-14, by huffman
generalize constant 'lim' and limit uniqueness theorems to class t2_space
2011-08-14, by huffman
Quotient Package: make quotient_type work with separate set type
2011-08-16, by Cezary Kaliszyk
updated README;
2011-08-15, by wenzelm
touch descendants of edited nodes;
2011-08-15, by wenzelm
parellel scheduling of node edits and execution;
2011-08-15, by wenzelm
tuned error message;
2011-08-15, by wenzelm
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
2011-08-15, by wenzelm
explicit check of finished evaluation;
2011-08-15, by wenzelm
refined Document.edit: less stateful update via Graph.schedule;
2011-08-15, by wenzelm
simplified exec: eliminated unused status flag;
2011-08-15, by wenzelm
consistently use variable name 'F' for filters
2011-08-14, by huffman
generalize lemmas about LIM and LIMSEQ to tendsto
2011-08-14, by huffman
HOL-Nominal-Examples: respect distinction between sets and functions
2011-08-13, by huffman
less verbosity in batch mode -- spam reduction and notable performance improvement;
2011-08-13, by wenzelm
merged
2011-08-13, by wenzelm
HOL-Hahn_Banach: use Set_Algebras library
2011-08-13, by huffman
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
2011-08-13, by huffman
clarified Toplevel.end_theory;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13, by wenzelm
provide node header via Scala layer;
2011-08-13, by wenzelm
reduced verbosity;
2011-08-13, by wenzelm
tuned signature;
2011-08-13, by wenzelm
clarified node header -- exclude master_dir;
2011-08-13, by wenzelm
tuned;
2011-08-13, by wenzelm
maintain node header;
2011-08-13, by wenzelm
removed unused lemma; removed old-style ;
2011-08-13, by kleing
point isatest-statistics to the right afp log files
2011-08-13, by kleing
IMP/Util distinguishes between sets and functions again; imported only where used.
2011-08-13, by kleing
remove redundant lemma setsum_norm in favor of norm_setsum;
2011-08-12, by huffman
merged
2011-08-12, by huffman
make more HOL theories work with separate set type
2011-08-12, by huffman
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
2011-08-13, by wenzelm
merged
2011-08-12, by wenzelm
merged
2011-08-12, by huffman
make Multivariate_Analysis work with separate set type
2011-08-12, by huffman
make HOLCF work with separate set type
2011-08-12, by huffman
merged
2011-08-12, by huffman
avoid duplicate rule warnings
2011-08-11, by huffman
modify euclidean_space class to include basis set
2011-08-11, by huffman
remove lemma stupid_ext
2011-08-11, by huffman
documented extended version of case_names attribute
2011-08-12, by nipkow
normalized theory dependencies wrt. file_store;
2011-08-12, by wenzelm
general Graph.schedule;
2011-08-12, by wenzelm
allow "$" within basic path elements (NB: initial "$" refers to path variable);
2011-08-12, by wenzelm
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-12, by wenzelm
simplified class Thy_Header;
2011-08-12, by wenzelm
clarified Exn.message;
2011-08-12, by wenzelm
uniform treatment of header edits as document edits;
2011-08-11, by wenzelm
explicit datatypes for document node edits;
2011-08-11, by wenzelm
tuned;
2011-08-11, by wenzelm
disentangled nested ML files;
2011-08-11, by wenzelm
minimal script to run raw Poly/ML with concurrency library;
2011-08-11, by wenzelm
somewhat more uniform THIS;
2011-08-11, by wenzelm
more trimming;
2011-08-11, by wenzelm
recovered some ML toplevel pp;
2011-08-11, by wenzelm
some trimming;
2011-08-11, by wenzelm
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
2011-08-11, by wenzelm
redundant use of misc_legacy.ML;
2011-08-11, by wenzelm
eliminated use of recdef
2011-08-11, by krauss
removed obsolete recdef-related examples
2011-08-11, by krauss
removed unused material, which does not really belong here
2011-08-11, by krauss
merged
2011-08-10, by huffman
avoid warnings about duplicate rules
2011-08-10, by huffman
follow standard naming scheme for sgn_vec_def
2011-08-10, by huffman
remove several redundant and unused theorems about derivatives
2011-08-10, by huffman
remove redundant lemma
2011-08-10, by huffman
simplify proof of lemma bounded_component
2011-08-10, by huffman
simplify some proofs
2011-08-10, by huffman
more uniform naming scheme for finite cartesian product type and related theorems
2011-08-10, by huffman
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
2011-08-10, by huffman
merged
2011-08-10, by wenzelm
split Linear_Algebra.thy from Euclidean_Space.thy
2011-08-10, by huffman
full import paths
2011-08-10, by huffman
declare tendsto_const [intro] (accidentally removed in 230a8665c919)
2011-08-10, by huffman
merged
2011-08-10, by huffman
simplified definition of class euclidean_space;
2011-08-10, by huffman
bounded_linear interpretation for euclidean_component
2011-08-09, by huffman
lemma bounded_linear_intro
2011-08-09, by huffman
avoid duplicate rewrite warnings
2011-08-09, by huffman
mark some redundant theorems as legacy
2011-08-09, by huffman
Derivative.thy: more sensible subsection headings
2011-08-09, by huffman
Derivative.thy: clean up formatting
2011-08-09, by huffman