remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc

remove unused lemmas

simplify proofs

make uses of bin_sign respect int/bin distinction

removed unnecessary lemma zero_bintrunc

remove unnecessary lemmas

removed unnecessary constant bin_rl

remove duplication of lemmas bin_{rest,last}_BIT

remove lemmas Bit{0,1}_div2

simplify proof

deal with FIXMEs for linarith examples

CONTRIBUTORS

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

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;