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

merged

added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall

avoid *** in normal output, which usually marks errors in logs

added Markup.Name and Markup.Kind convenience; token_style for entity kind markup;

decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;

tuned signatures;

decode_term: more precise reports;

adhoc token style for free/bound;

decode_term/disambig: report resolved term variables for the unique (!) result;

removed unclear comments stemming from ed24ba6f69aa;

present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

added Future.cond_forks convenience;

Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;

tuned;

more direct loose_bvar1; tuned; slight re-unification of clone (cf. 47f8bfe0f597);

suppress Mercurial backup files; uniform treatment of tool filtering in bash/perl/scala;

updated generated file; tuned whitespace;

merged

SML_makeall: run with -j 3

fixed incomplete rename (1cdf54e845fa)

eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)

merged

changing iteration scheme of functions to use minimal number of function updates for exhaustive testing

added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)

mira interface to 'isabelle make' in addition to usedir and makeall; do not require dependencies

clarified

parameterize configurations by custom settings

Change coercion for RealDef to use function application (not composition)

revisiting Code_Prolog (cf. 6fe4abb9437b)

fixed postprocessing for term presentation in quickcheck; tuned spacing

enable Z3 in the test configuration

add "-?" to "nitrox" tool

clean up new Skolemizer code -- some old hacks are no longer necessary

specify proper defaults for Nitpick and Refute on TPTP + tuning