tuned;

merged

merged

Fixed bugs: - set_env no longer modifies pfuns field in theory data record. Instead, a copy of this field is now contained in the env field. - add_type_def now checks whether type associated with SPARK enumeration type is really a datatype with no parameters. - check_pfuns_types now properly strips off prefixes of proof function names.

merged

subtype preprocessing in Quickcheck; adding option use_subtype; tuned

adding parsing of an optional predicate with quickcheck_generator command

updated generated files (cf. 8d51b375e926);

merged;

add missing lemmas to compute_div_mod

remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)

avoid using constant Int.neg

renamed ex/Numeral.thy to ex/Numeral_Representation.thy

reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems

tuned whitespace

tuned proof

tuned proof

distributed lattice properties of predicates to places of instantiation

removing some unnecessary premises from Divides

simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)

observe HEIGHT of overview ticks; misc tuning and clarification;

more careful painting of overview component: more precise and more efficient;

clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;

use qualified constant names instead of suffixes (from Florian Haftmann)

tuned proofs

tuned

brute-force adjustion

tuned whitespace