init options on startup as well;

theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;

tuned: use induction rule sigma_sets_induct_disjoint

tuned FinMap

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

more refs;

isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release); always generate sty files, as before c5d0f19ef7cb;

proper jvmpath for windows;

more generous tracing_limit, with explicit system option;

adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;

update options via protocol; jEdit dialog for "Parallel Checking" options;

more accurate pixel_range -- do not round offset here;

tuned signature;

prefer absolute default $USER_HOME/Scratch.thy;

more portable process exit;

tuned -- eliminate pointless ML method definition;

tuned;

NEWS;

tuned structure of Isabelle/HOL;

method setup for Classical steps;

tuned signature;

updated keywords;

moved (b)choice_iff(') to Hilbert_Choice

move theorems to be more generally useable

merged

made SML/NJ happy;

renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space

renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

measurability for nat_case and comb_seq

rules for AE and prob

rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication

more measurability rules

renamed to more appropriate lim_P for projective limit

allow arbitrary enumerations of basis in locale for generation of borel sets

repaired slip accidentally introduced in 57209cfbf16b

prefer implementation in HOL; n.b. code_reflect cannot reflect type synonyms

corrected headers

hide constants of auxiliary type finmap

generalized to copy of countable types instead of instantiation of nat for discrete topology

added projective limit; proof is based on auxiliary type finmap::polish_space

regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards

tuned -- eliminated obsolete citation of isabelle-ref;

updated basic equality rules;

removed somewhat pointless historic material;

updated unification options;

removed some historic material that is obsolete or rarely used;

tuned;

updated section on ordered rewriting;

updated subgoaler/solver/looper;

removed somewhat pointless historic material; tuned;

tuned;

updated explanation of rewrite rules;

(re)moved old material about Simplifier;

some coverage of "resolution without lifting", which should be normally avoided;

removed somewhat pointless historic material;

updated biresolve_tac, bimatch_tac; removed obscure historical material;

moved classical wrappers to IsarRef; removed somewhat pointless historic material;

avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");

updated citations;

tuned;

removed junk;

removed pointless historic material;

more on Simplifier rules, based on old material;

refurbished Simplifier examples;

more on the Simplifier, based on old material;

more concise/precise documentation;

tuned text

replaced relation by function - simplifies development

made SMLNJ happier

import Sublist rather than PrefixOrder to avoid unnecessary class instantiation

prefer explicit Random.seed

dropped dead code

tuned import order

tuned layout

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

create temp directory if not already created

merged

new theory IMP/Finite_Reachable

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

thread context correctly when printing backquoted facts

dropped dead code; tuned theory text

modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)

merged

fixed underscores

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

assume probability spaces; allow empty index set

added projective_family; generalized generator in product_prob_space to projective_family

moved lemmas further up

tuned proofs

using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier

hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call

NEWS

rewriting with the simpset that is passed to the simproc

handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc

tuned

syntactic tuning and restructuring of set_comprehension_pointfree simproc

using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls

improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones

adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc

handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc

simplified structure of patterns in set_comprehension_simproc

refined stack of library theories implementing int and/or nat by target language numerals

restored SML code check which got unintentionally broken: must explicitly check for error during compilation; restore more conventional namespace during check (relevant for Imperative-HOL)

add support for function application to measurability prover

renamed Sledgehammer option

always show timing for structured proofs

use implications rather than disjunctions to improve readability

avoid name clashes

fixed more "Trueprop" issues

removed needless sort

avoid double "Trueprop"s

use original formulas for hypotheses and conclusion to avoid mismatches

track formula roles in proofs and use that to determine whether the conjecture should be negated or not

correct parsing of E dependencies

proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction

tuned

code for while directly, not via while_option