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;

Path.split convenience;

get theory from last executation state; tuned error messages;

explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example); reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);

clarified cancel_execution/await_cancellation;

tuned signature; tuned;

tuned;

re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target

Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);

quasi-static Isabelle_System -- reduced tendency towards "functorial style";

explicit class Counter;

merged

the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})

equalities of subsets of atLeastLessThan

adding documentation of the value antiquotation to the code generation manual

make SML/NJ happy

install case certificate for If after code_datatype declaration for bool

tuned typo

pervasive Basic_Library in Scala; tuned;

some support for theory files within Isabelle/Scala session;

imitate exception ERROR of Isabelle/ML;

eliminated null;

more explicit edit_node vs. init_node; some support for master_dir and header;

tuned signature;

Thy_Header.read convenience;

some support for Session.File_Store;

tuned signature;

eliminated redundant session_ready;

tuned;

uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;

misc tuning;

correction: do not assume that case const index covered all cases

remove illegal case combinators after merge

corrected misunderstanding what `old functions` are supposed to be

centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be

merged

index cases for constructors