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;

more antiquotations;

tuned whitespace;

eliminated some legacy operations;

removed dead code, which has never been active in recorded history;

do not open ML structures;

tuned signature;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

adapting exhaustive generators in record package

outputing if counterexample is potentially spurious or not

making catch_match polymorphic

compilations return genuine flag to quickcheck framework

extending quickcheck's result by the genuine flag

reporting random compilation also catches match exceptions internally

the narrowing also indicates if counterexample is potentially spurious

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not