Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;

give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)

merged

coercions

merged

moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.

Corrected IsaMakefile

merged

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

merged

merged

change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec

add lemma cont2cont_if_bottom

added Parse.literal_fact with proper inner_syntax markup (source position); tuned;

tuned signature;

less frequent sidekick parsing, which is relatively slow;

basic setup for bundled Java runtime;

updated reference platforms;

merged

merged

gave more standard finite set rules simp and intro attribute

more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);

added 'syntax_declaration' command;

more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;

superficial tuning;

updated versions;

recovered Isabelle2009-2 NEWS -- published part is read-only;

follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);

removed HOLCF for now as explicit component

fix cut-and-paste errors for HOLCF entries in IsaMakefile

update web description of HOLCF; fix broken link to HOLCF/index.html

remove HOLCF from build script, since it no longer works

moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;

merged

rename Pcpodef.thy to Cpodef.thy; rename pcpodef.ML to cpodef.ML;

renamed several HOLCF theorems (listed in NEWS)

rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo

rename rep_contlub lemmas to rep_lub

rename function 'match_UU' to 'match_bottom'

rename function 'strict' to 'seq', which is its name in Haskell

merged

merged

typscheme with signatures is inappropriate when building empty certificate; prefer logical_typscheme over const_typargs; tuned

merged

merged

corrected: use canonical variables of type scheme uniformly

tuned

merged

consider sort constraints for datatype constructors when constructing the empty equation certificate; actually consider sort constraints in constructor sets; dropped redundant bindings

tuned example

merged

updated generated documents

added equation for Queue; tuned proofs

added evaluation section

tuned formatting; adjustments to changes on ML level

added label

more thorough process termination (cf. Scala version);