avoid Collect_def in proof

modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;

improved default context for ML toplevel pretty-printing;

less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);

some convenience actions/shortcuts for control symbols;

export Function_Fun.fun_config for user convenience;

moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

distinguish THF syntax with and without choice (Satallax vs. LEO-II)

merged

add simp rules for isCont

updated keywords -- old codegen is no longer in Pure;

include HOL-Library keywords for the sake of recdef;

merged

Multivariate_Analysis includes Determinants.thy, but doesn't import it by default

get Multivariate_Analysis/Determinants.thy compiled and working again

get Library/Permutations.thy compiled and working again

workaround for Cygwin, to make it work in the important special case without extra files;

more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;

tuned message;

more robust treatment of node dependencies in incremental edits;

use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;

omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;

merged

generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space

add lemma tendsto_compose

remove extraneous subsection heading

generalized lemma closed_Collect_eq

remove duplicate lemma disjoint_iff

Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space

add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;

generalize lemma continuous_uniform_limit to class metric_space

remove duplicate lemmas eventually_conjI, eventually_and, eventually_false

Topology_Euclidean_Space.thy: organize section headings

simplify some proofs

generalize lemma convergent_subseq_convergent

locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses

locale-ize some constant definitions, so complete_space can inherit from metric_space

generalize constant 'lim' and limit uniqueness theorems to class t2_space

Quotient Package: make quotient_type work with separate set type

updated README;

touch descendants of edited nodes; more precise handling of Graph exceptions;

parellel scheduling of node edits and execution;

tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

HOL-Nominal-Examples: respect distinction between sets and functions

less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;

merged

HOL-Hahn_Banach: use Set_Algebras library

ex/Quickcheck_Examples.thy: respect distinction between sets and functions

clarified Toplevel.end_theory;

simplified Toplevel.init_theory: discontinued special name argument;

simplified Toplevel.init_theory: discontinued special master argument;

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;

reduced verbosity;

tuned signature;

clarified node header -- exclude master_dir;

tuned;

maintain node header; misc tuning and clarification;

removed unused lemma; removed old-style ;

point isatest-statistics to the right afp log files

IMP/Util distinguishes between sets and functions again; imported only where used.

remove redundant lemma setsum_norm in favor of norm_setsum; remove finiteness assumption from setsum_norm_le;

merged

make more HOL theories work with separate set type

immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown;

merged

merged

make Multivariate_Analysis work with separate set type

make HOLCF work with separate set type

merged

avoid duplicate rule warnings

modify euclidean_space class to include basis set

remove lemma stupid_ext

documented extended version of case_names attribute

normalized theory dependencies wrt. file_store;

general Graph.schedule;

allow "$" within basic path elements (NB: initial "$" refers to path variable);

clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

simplified class Thy_Header;

clarified Exn.message;

uniform treatment of header edits as document edits;

explicit datatypes for document node edits;

tuned;

disentangled nested ML files;

minimal script to run raw Poly/ML with concurrency library;

somewhat more uniform THIS;

more trimming;

recovered some ML toplevel pp;

some trimming;

prefix of Pure/ROOT.ML required for concurrency within the ML runtime;

redundant use of misc_legacy.ML;

eliminated use of recdef

removed obsolete recdef-related examples

removed unused material, which does not really belong here

merged

avoid warnings about duplicate rules

follow standard naming scheme for sgn_vec_def

remove several redundant and unused theorems about derivatives

remove redundant lemma

simplify proof of lemma bounded_component

simplify some proofs

more uniform naming scheme for finite cartesian product type and related theorems

move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy

merged

split Linear_Algebra.thy from Euclidean_Space.thy

full import paths

declare tendsto_const [intro] (accidentally removed in 230a8665c919)

merged

simplified definition of class euclidean_space; removed classes real_basis and real_basis_with_inner

bounded_linear interpretation for euclidean_component

lemma bounded_linear_intro

avoid duplicate rewrite warnings

mark some redundant theorems as legacy

Derivative.thy: more sensible subsection headings

Derivative.thy: clean up formatting