Generic parsers for Isabelle/Isar outer syntax -- Scala version.

class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure; added Token_Reader; tuned;

Changes in generated code, apparently caused by changes to the code generation system itself.

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;