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);

added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;

names for control symbols without "^", which is relevant for completion;

some unicode chars for special control symbols;

tuned;

tuned markup;

avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;

proper gfx.setColor;

proper x1; tuned;

convenience functions;

more robust caret painting wrt. surrogate characters; discontinued glyphvector drawing -- less special cases;

do not control malformed symbols;

Buffer.editSyntaxStyle: mask extended syntax styles;

hardwired abbreviations for standard control symbols;

updated to jedit_build-20110618, which is required for sub/superscript rendering;

basic support for extended syntax styles: sub/superscript;

tuned -- Map.empty serves as partial function;

proper place for config files (cf. 55866987a7d9);

tuned signature;

merged

IMP compiler with int, added reverse soundness direction

proper place for config files;

tuned markup;

highlight via foreground painter, using alpha channel;

tuned signature;

tuned text;

inner literal/delimiter corresponds to outer keyword/operator;

tuned markup;

more uniform treatment of "keyword" vs. "operator";

simplified Line_Context (again);

more robust treatment of partial range restriction;

select_markup: no filtering here -- results may be distorted anyway;

more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;

more explicit error message; convert/revert range; tuned;

merged

gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"

added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users

fixed soundness bug related to extensionality

unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);

flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);

recovered markup for non-alphabetic keywords;

more precise imitation of original TextAreaPainter: no locking;

more precise imitatation of original TokenMarker: no locking, interned context etc.;

brute-force range restriction to avoid spurious crashes;

static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);

explicit dependency on Pure.jar;

partial scans of nested comments;

some support for partial scans with explicit context; clarified junk vs. junk1;

tuned spelling

updated generated file;

merged

spelling

avoid compiler warning -- this is unchecked anyway;

tuned messages;

uniform use of Document_View.robust_body;

merged

merge

fixed soundness bug made more visible by previous change

use more appropriate type systems for ATP exporter

type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases

more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);

more robust init;

recovered orig_text_painter from f4141da52e92;