merged

explicit code equation for equality

tuned error messages;

tuned;

tuned signature -- corresponding to Scala version;

made SML/NJ happy; tuned error;

more uniform padded_markup, which is important for caret visibility despite absence of markup;

merged

merged

tuned proofs

tuned notation

tuned notation

tuned notation

NEWS;

proper InvocationTargetException.getCause for indirect exceptions; capture hard errors to ensure protocol integrity; tuned error messages;

tuned error message;

tuned signature;

JVM method invocation service via Scala layer;

tuned signature;

some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;

tuned XML.Cache parameters;

some support to invoke Scala methods under program control;

merged;

merged

tuned proofs and notation

more succinct proofs

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

rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq

improved translation of lambdas in THF

added generation of lambdas in THF

add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)

simplified Symbol.iterator: produce strings, which are mostly preallocated; eliminated Symbol.CharSequence complications;

tuned comment (cf. e9f26e66692d);

Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;

theory name needs to conform to Path syntax;

hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;

prefer space_explode/split_lines as in Isabelle/ML;