overview.delay_repaint: avoid wasting GUI cycles via update_delay; prefer delay_first for prover initiated events -- avoid indefinite delay;

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

tuned

tuned

tuned code

dropped whitespace

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

corrected typo

dropped dead code

notepad is more appropriate here

corrected treatment of applications of built-in functions to higher-order terms

NEWS

merged

added congruence rules for Option.{map|bind}

updated generated documents

avoid redefinition of @{theory} antiquotation

update of generated documents

tuned whitespace

clarified

corrected spelling

clarified

more precise semantics of "theory" antiquotation

tuned import

dropped references to obsolete theories

adjusted to set type constructor

tuned whitespace

more explicit error on malformed abstract equation; dropped dead code; tuned signature

simplified configuration options for syntax ambiguity;