observe distinction between sets and predicates more properly

moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace

avoid case-sensitive name for example theory

merged

case_names NEWS

adding documentation about simps equation in the inductive package

activating narrowing-based quickcheck by default

more precise treatment of exception nesting and serial numbers;

more careful treatment of exception serial numbers, with propagation to message channel;

updated sequential version (cf. b94951f06e48);

tuned comments;

tuned document; tuned proofs;

clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;

export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;

tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;

Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.

merged

HOL-IMP: respect set/pred distinction

Determinants.thy: avoid using mem_def/Collect_def

Wfrec.thy: respect set/pred distinction

follow updates of Isabelle/Pure;

merged

IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library

merged

Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems

add lemma tendsto_compose_eventually; use it to shorten some proofs

Topology_Euclidean_Space.thy: simplify some proofs

add lemma metric_tendsto_imp_tendsto

simplify proofs of lemmas open_interval, closed_interval

identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;

clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;

more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

tuned signature;

merged

merged

merged

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;