merged

tuned whitespace

tuned whitespace

adding documentation about find_unused_assms command and use_subtype option in the IsarRef

NEWS

adding some examples with find_unused_assms command

adding new command "find_unused_assms"

removing some unnecessary premises from Map theory

preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)

generalizing inj_on_Int

moving Quickcheck's example to its own session

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