tuned XML modules;

Quotient example: Lists with distinct elements

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;

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

cover induct's "arbitrary" more deeply

merged;

enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes

made minimizer informative output accurate

test a few more type encodings

further repair "mangled_tags", now that tags are also mangled

update documentation after "type_enc" renaming + fixed a few other out-of-date factlets

renamed "type_sys" to "type_enc", which is more accurate

document "simple_higher" type encoding

cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company

mangle "ti" tags

tuning

clarified Thy_Syntax.element;

tuned layout;

proper @{binding} antiquotations (relevant for formal references);

tuned;

merged

reverted 782991e4180d: fold_fields was never used

reverted ce00462f,b3759dce, 7a165592: unwanted generalisation

improving actual dependencies

adding a minimalistic documentation of the value antiquotation in the Isar reference manual

adding a value antiquotation

more general theory header parsing;

back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);

merged

parse term in auxiliary context augmented with variable; pass through binding appropriately; more standard syntax and ML interface

linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages); control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)

prefer Isabelle path algebra;

proper fold order;

more Path operations; tuned signature;

getenv_strict in ML; tuned;

standardized use of Path operations;

tuned comments;

abstract algebra of file paths in Scala (cf. path.ML);

proper Path.print;

basic operations on lists and strings;

tuned signature;

simplified/unified Simplifier.mk_solver;

modernized some simproc setup;

modernized some simproc setup;

print Path.T with some markup;

HTML: render control symbols more like Isabelle/Scala/jEdit;

collapse map functions with identity subcoercions to identities;

reenabled accidentally-disabled automatic minimization

tuned markup;

merged

tidied messy proofs

merged

adding timeout to quickcheck narrowing

simplified proofs using metis calls

merged

keyfree: The set of key-free messages (and associated theorems)

merged

new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics

added reference for MESON

document "meson" and "metis" in HOL specific section of the Isar ref manual

clarify minimizer output

don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical

tweaked comment

document "sound" option

minor Sledgehammer news

added "sound" option to force Sledgehammer to be pedantically sound

removed "full_types" option from documentation

document changes to Sledgehammer and "try"

removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway

clarify warning message to avoid confusing beginners

remove experimental trimming feature -- it slowed down things on Linux for some reason

filter out some tautologies using an ATP, especially for those theories that are known for producing such things

NEWS;

document antiquotations are managed as theory data, with proper name space and entity markup;

proper checking of @{ML_antiquotation};

hide rather short auxiliary names, which can easily occur in user theories;

updated generated file;

ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;

old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;

parallel Syntax.parse, which is rather slow;

markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";

move conditional expectation to its own theory file

updated SMT certificates

generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem); maintain extra-logical information when introducing explicit application; handle let-expressions properly

proper tokens only if session is ready;

entity markup for "type", "constant";

clarified Markup.CLASS vs. HTML.CLASS;

tuned color, to avoid confusion with type variables;

discontinued generic XML markup -- this is for XHTML with <span/> elements;

type classes: entity markup instead of old-style token markup;

clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;

clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example; discontinued unused Binding.qualified_name_of;

produce string constant directly;

merged

While reading equations of an interpretation, already allow syntax provided by the interpretation base.

removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;

clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);

CLASSPATH already converted in isabelle java wrapper;

removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;

more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!

clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);

more robust concurrent builds;

merged

add countable_datatype method for proving countable class instances

merged;

instance inat :: number_semiring

added number_semiring class, plus a few new lemmas; no changes to the simpset yet

merged

fiddle with remote ATP settings, based on Judgment Day

give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers