Updated NEWS

More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.

Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.

merged

use type constructor as name for variable

optional explicit prefix for type mapper theorems

file for package tool type_mapper carries the same name as its Isar command

merged

domain package generates non-authentic syntax rules for parsing only

builtin time bounds (again);

tuned;

more abstract handling of Time properties;

store tooltip-dismiss-delay as Double(seconds);

more abstract/uniform handling of time, preferring seconds as Double;

merged

NEWS

just one HOLogic.mk_comp;

more direct use of binder_types/body_type;

tuned;

simplified HOL.eq simproc matching;

tuned;

just one Term.dest_funT;

activate subtyping/coercions in theory Complex_Main;

simplified equality on pairs of types;

more precise dependencies;

two-staged architecture for subtyping; improved error messages of subtyping (using the new architecture); bugfix: constraint graph consistency check after cycle elimination;

merged

change cpodef-generated cont_Rep rules to cont2cont format

internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules

remove gratuitous semicolons from ML code

add continuity lemma for List.map

simplify predomain instances

merged

split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models

code preprocessor setup for numerals on word type; less meta-equalites; more xsymbols; less implicit propositions

merged

adaptions to changes in Equiv_Relation.thy

adapted fragile proof

adaptions to changes in Equiv_Relation.thy; prefer primrec if possible

adaptions to changes in Equiv_Relation.thy

merged

more systematic and compact proofs on type relation operators using natural deduction rules

adapted proofs to slightly changed definitions of congruent(2)

reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text

replaced slightly odd locale congruent2 by plain definition

replaced slightly odd locale congruent by plain definition

equivI has replaced equiv.intro

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules

moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition

simplify proof of LIMSEQ_unique

use new 'file' antiquotation for reference to Dedekind_Real.thy

merged

instance list :: (discrete_cpo) discrete_cpo; compactness lemmas for Nil, Cons; instance list :: (chfin) chfin;

merged

also support higher-order rules for Z3 proof reconstruction

merged

less ghc-specific pragma

tuned

updated generated files;

added document antiquotation @{file};

Parse.liberal_name for document antiquotations and attributes;

ML results: enter before printing (cf. Poly/ML SVN 1218);

merged