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

Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.

generalize lemmas power_number_of_even and power_number_of_odd

merged

add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis

simplified arrangement of jars;

adapted to Cygwin;

provide Isabelle/Scala environment as Java extension, instead of user classpath (which is subject to adhoc changes);

explicit import java.lang.System to prevent odd scope problems;

ensure export of initial CLASSPATH;

augment Java extension directories;

basic setup for Isabelle charset;

prefer actual charset over charset name;

clarified default ML settings;

lazy Isabelle_System.default supports implicit boot;

clarified plugin start/stop;

clarified init/exit procedure;

clarified decoded control symbols;

init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;

prefer STIXGeneral -- hard to tell if better or worse;

merged

export lambda-lifting code as there is potential use for it within Sledgehammer

updated to jedit-4.4.1 and jedit_build-20110622;

clarified chunk.offset, chunk.length;

avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);

some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;

more precise font transformations: shift sub/superscript, adjust size for user fonts; tuned;

don't change the way helpers are generated for the exporter's sake

provide appropriate type system and number of fact defaults for remote ATPs

order generated facts topologically

peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")

tweaked E, SPASS, Vampire setup based on latest Judgment Day results

remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations

avoid double ASCII-fication

make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity

generate type predicates for existentials/skolems, otherwise some problems might not be provable

insert rather than append special facts to make it less likely that they're truncated away

hidden font: full height makes cursor more visible;

more uniform treatment of recode_set/recode_map; HTML spans with user fonts;

tuned iteration over short symbols;

Symbol.is_ctrl: handle decoded version as well; clarified user font font index handling;

some support for user symbol fonts;

removed obsolete font specification;

more tolerant Symbol.decode;

simplified/generalized ISABELLE_FONTS handling;

updated to jedit_build-20110620;

added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;

clean up SPASS FLOTTER hack

remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers

only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded

slightly better setup for E

respect "really_all" argument, which is used by "ATP_Export"

slightly better setup for SPASS and Vampire as more results have come in

optimized SPASS and Vampire time slices, like E before

optimized E's time slicing, based on latest exhaustive Judgment Day results

deal with ATP time slices in a more flexible/robust fashion

literal unicode in README.html allows to copy/paste from Lobo output;

merged;

explain special control symbols;

accept control symbols;

fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies

recognize one more E failure message

tweaked TPTP formula kind for typing information used in the conjecture

more forceful message

treat quotes as non-controllable, to reduce surprise in incremental editing;

abbreviations for special control symbols;

completion for control symbols;

updated to jedit_build-20110619;

support for bold style within text buffer; hidden: white foreground;

tuned;

discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);