Polishing up the English

merged

merged

clarified various user-defined syntax issues

prefer prefix "iso" over potentially misleading "is"; tuned

moved lemmas o_eq_dest, o_eq_elim here

add 'morphisms' option to domain_isomorphism command

merged

generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs

rename equals_zero_I to minus_unique (keep old name too)

add lemma swap_triple

improve performance by reordering of parser combinators;

added nested comments; tuned;

more Scala sources;

simiplified result of keyword parser (again); sort completions by plain string order; moved Reverse to library.scala;

simplified result of keyword and symbols parser; some support for parsing outer syntax tokens;

Outer lexical syntax for Isabelle/Isar -- Scala version.

refined some Symbol operations/signatures; tuned;

refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;

added basic library -- Scala version; added extra support for exceptions -- Scala version; moved exn.ML to accompany exn.scala;

indicate final state of keywords; added symbol scanner;

added symbol classification; tuned;

tuned;

merged

imitate PG style;

merged

imitate PG colors;

made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default; up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option

merged

polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation

merged

added support for binary nat/int representation to Nitpick

distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick; this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on

merged

get rid of polymorphic equality in Nitpick's code + a few minor cleanups

added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections

markup bad YXML as malformed; removed unused XML.document; removed unused markup;

replace invalid code points -- instead of exception;

tuned signature;

removed junk (cf. f49d45afa634);

merged

merged

add lemma INFM_conjI

added lemmas about INFM/MOST

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

streamlined proofs

fixed typo

merged

only invoke metisFT if metis failed

added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas

merged

each import resides in its own line

using existing lattice classes

added get_data;

sealed XML.Tree; keep original XML.Tree within DOM as user data;

simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway);

slightly more robust and less ambitious version of install_fonts;