context/theory parametres tuned

maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types

add induction rule for list_all2

deactivating quickcheck_narrowing if Efficient_Nat theory is loaded

tuned quickcheck's response

more systematic lemma name

adding examples for quickcheck narrowing about partial functions

removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions

HOLCF/ex/Letrec.thy: keep class 'domain' as default sort

more error checking for fixrec

reinstate old functions cfst and csnd as abbreviations

merged

tuned

merged

added a specific tactic and method that deal with partial equivalence relations

use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts

avoid multiple TFF1 declarations

updated TFF1 support

updated Metis to 20110926 version

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead

add cancellation simprocs for type enat

tuned

increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure

tuned proofs

added lemmas

tuned proof

real is better supported than real_of_nat, use it in the nat => ereal coercion

merged

the note about morphisms moved in the description part

updating documentation about quiet and verbose options in quickcheck

making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples

adding verbose configuration to quickcheck

random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument

the reporting random testing also returns if the counterexample is genuine or potentially spurious

exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly

inverted flag potential to genuine_only in the quickcheck narrowing Haskell code

NEWS

documenting the genuine_only option in quickcheck;

renaming potential flag to genuine_only flag with an inverse semantics

quickcheck narrowing continues searching after found a potentially spurious counterexample

outputing the potentially spurious counterexample and continue search

dynamic genuine_flag in compilation of random and exhaustive

indicating where the restart should occur; making safe_if dynamic

merged

enforce parantheses around SKIP {_}

adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

merged

remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality

missing dependency

improved var names

invariant holds before loop

caret_range based on BreakIterator, which handles combined unicode characters as well;

misc tuning;

some localization;

eliminated some legacy operations;