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

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

added "nitrox" tool (Nitpick for first-order TPTP problems) to components

made one more Metis example use the new Skolemizer

Metis examples use the new Skolemizer to test it

new version of Metis 2.3 (29 Dec. 2010)

remove newly added wrong logic

more precise failure reporting in Sledgehammer/SMT

avoid evil "export_without_context", which breaks if there are local "fixes"

more robust handling of variables in new Skolemizer

merged

added subsection on Scala specialities

added more judgement day provers

allowing special set comprehensions in values command; adding an example for special set comprehension in values

merged

adding documentation about the eval option in quickcheck

adapting Quickcheck_Prolog to latest changes

changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth

adapting mutabelle; exporting more Quickcheck functions

making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck

changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout

added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;

tuned;

dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

more direct loose_bvar1; tuned;

indentation;

update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);

added editor mode line;

isolate change of Proofterm.proofs in TPTP.thy from rest of session; qualified Proofterm.proofs to facilitate grepping;

list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin; exclude backup files;

updated contributed components

Z3 non-commercial usage may explicitly be declined

export status function to query whether Z3 has been activated for usage within Isabelle