more succinct proofs

adding a very liberal timeout for values after a test case failed due to the restricted timeout

improved NEWS

NEWS

standardized String.concat towards implode (cf. c37a1f29bbc0)

adding quickcheck examples for evaluating floor and ceiling functions

adding code equations to execute floor and ceiling on rational and real numbers

adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;

lambda terms with XML data representation in Scala; avoid `class` in signature;

XML data representation of lambda terms;

YXML.string_of_body convenience;

made SML/NJ happy;

tuned signature;

more abstract signature; tuned;

simplified XML_Data;

less currying in Scala;

propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;

echo prover input via raw_messages, for improved protocol tracing;

tuned;

tuned signature;

clarified propagation of node name and header;

more precise treatment of prover definedness;

tuned source structure;

some support for blobs (arbitrary text files) within document nodes;

tuned signature;

moved global state to structure Document (again);

moved Outer_Syntax.load_thy to Thy_Load.load_thy; tuned signatures; tuned module dependencies;

less stateful outer_syntax;

discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;

discontinued special treatment of hard tabulators;

eliminated hard tabs;

merged

merged

added translation to fix critical pair between abbreviations for surj and ~=

floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling

standardized String.concat towards implode;

more abstract Thy_Load.load_file/use_file for external theory resources; prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;

comment;

clarified Thy_Load.digest_file -- read ML files only once;

tuned signature;

simplified make_option/dest_option; added make_variant/dest_variant -- usual representation of datatypes;

explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;

explicit indication of type Symbol.Symbol;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;

merged

make SML/NJ happier

make SML/NJ happy + tuning

moved ATP dependencies to HOL-Plain, where they belong

better setup for experimental "z3_atp"

64bit versions of some mira configurations

removed unused mira configuration

merged

tuning options to avoid spurious isabelle test failures

clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;

prefer Synchronized.var;

tuned errors; more direct Name.uu_ for dummy abstractions;

record package: proper configuration options;

just one copy of split_args; tuned error message;

merged