refactoring generator definition in quickcheck and removing clone

use the proper contexts/simpsets/etc. in the TPTP proof method

merged

make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option

merged

Deletion of all semicolons, because they interfere with Proof General

raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

tuned proofs

tuned proof

direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;

added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;

show more tooltip/sub-expression markup;

show tooltip/sub-expression for entity markup;

merged

remove unnecessary prob_preserving

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

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