merged Crude_Executable_Set into Executable_Set

merged

avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy"); this produces two copies of the same module, with separate references etc.

better error message in Refute when specifying a non-existing SAT solver

merged

updated certificate

merged

repaired read_const_expr, broken in 1e7ca47c6c3d

merged

verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization), custom-made (top-down) atomize_conv, store predicate and function symbols in a table instead of a list for faster lookup, updated certificates

merged

tuned proofs

tuned lattices theory fragements; generlized some lemmas from sets to lattices

avoid lazy val with side-effects -- spurious null pointers!?

toString: more robust handling of null; tuned;

proper markup text for loc;

output_syms: permissive treatment of control symbols, cf. Scala version;

basic treatment of special control symbols; misc tuning;

elements: more convenient result;

more robust treatment of line breaks -- Java "split" has off semantics;

added auxiliary constructors;

added elements: Interator; first isHighSurrogate, not isLowSurrogate; misc tuning and generalization;

merged

merged

tuned whitespace

merged, resolving minor conflicts

NEWS