add prob_space_vimage

use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);

fixed accidental redefinition

save reflexivity steps in discharging Z3 Skolemization hypotheses

adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall

adding general interface for batch validators in quickcheck

remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428

scheduler for judgement day

re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end

make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

merged

adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy

raised timeouts further, for SML/NJ

adapted parsing of session timing (cf. e86b10c68f0b)

merged

adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily

provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)

temporary workaround: filter out spurious monomorphic instances

added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default

added support for "dest:" to "try"

corrected infix precedence for boolean operators in Haskell

merged

removing dead code in exhaustive_generators

removing junk that should not have been committed

modernized specifications;

accomodate autofix discipline of non-body context;

session timing: show pseudo-speedup factor;

visualize skolem and hilite (undeclared frees); tuned colors;

more informative markup_free;

inline lemmas instead of accidental physical addressing -- explicit is better than implicit;

tuned white space and indentation; observe strict line length limitation (80-100 chars);

actually check list comprehension examples;

products of probability measures are probability measures

real multiplication is continuous

add lebesgue_real_affine

renewing specifications in HOL: replacing types by type_synonym

moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure

adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape

NEWS

generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities

merged

added missing smlnj target

modernized specifications -- less axioms;

modernized specifications -- some attempts to avoid wild axiomatizations; comp: retain infix \<circ> to retain type "o" from FOL; tuned proofs;

tuned proofs;

use shared copy of hoare_syntax.ML; misc tuning;

Hoare syntax: standard abstraction syntax admits source positions; re-unified some clones (!);

tuned headers;

tuned headers;

NEWS

rename Probability_Space to Probability_Measure

add infinite product measure

split Product_Measure into Binary_Product_Measure and Finite_Product_Measure

proved caratheodory_empty_continuous

list comprehension: strip positions where the translation cannot handle them right now;

address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;

raised various timeouts to accommodate sluggish SML/NJ

changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ

keep smlnj HOL images around