add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff

add lemmas open_image_fst, open_image_snd

Result.cache;

cache for partial sharing;

merged

Two new theorems about cardinality

replace 'UNIV - S' with '- S'

re-state lemmas using 'range'

make proof use only abstract properties of eventually

swap_self already declared [simp]

declare swap_self [simp], add lemma comp_swap

fifo: raw byte stream; Result: fully decoded symbols and tree structure; adapted to simplified message format; tuned;

added decode_chars, with raw character view on byte buffer and adhoc decoding via toString; parse/chunks: avoid direct string comparison, to make it actually work with abstract CharSequence;

tuned signature;

tuned;

simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;

robust representation of low ASCII control characters within XML/YXML text;

merged

filter out identical completions;

spaces not allowed, unfortunately

user aliasses

merged

replaced blast by metis (blast hangs with polyml-5.2)

avoid negative indices as argument ot drop

Upgraded a warning to an error

merged

improved crude deriving_show inference

explicit name for function space

make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits

make Nitpick "Core" test more conservative, to avoid problems on Larry's machine

made sml/nj happy

also sort verification conditions before printing

print assertions in a more natural order

removed unique ids -- now in session.scala;

merged

Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;

Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;

merged

repaired accident: do not forget module contents if there are no imports

option width for Code_Target.code_of

default_code_width is now proper theory data

merged

updated dependencies

make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations

depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)

merged

moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)

avoid dependency on implicit dest rule predicate1D in proofs

merged

NEWS

merged

merged

take and drop as projections of chop

explicit lower bound for index

merged

merged