tuned proofs;

more robust visible_range: allow empty view;

misc tuning;

merged;

made SML/NJ happy;

tuned proofs;

merged

tuned proofs;

approximate Perspective.full within the bounds of the JVM;

misc tuning; more indentation;

invoke later to reduce chance of causing deadlock;

misc tuning; more indentation;

separate module for text status overview;

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