support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)

tuning

NEWS;

merged

restrict node_required status and Theories panel to actual theories;

ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;

tuned;

refer to thy_load command of auxiliary file;

proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;

load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;

tuned;

more explicit indication of missing files;

more uniform handling of inlined files;

tuned signature;

clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;

release file errors at runtime: Command.eval instead of Command.read;

maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;

always reparse nodes with thy_load commands, to update inlined files;

proper Thy_Load.append of auxiliary file names; inlined errors;

proper theory name vs. node name;

clarified boundary cases of Document.Node.Name;

clarified Thy_Load.node_name;

inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;

persistent value;

caching of blob; precise file content according to jEdit IO;

tuned;

maintain document model for all files, with document view for theory only, and special blob for non-theory files;

tuned

whitespace tuning

tuning

more refactoring to accommodate SMT proofs

tuning

tuning

more correct NEWS

simplified old code

refactoring

refactoring

merged

BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate

add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

refactored

updated docs

use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'

prefix internal names as well

case_if -> case_eq_if + docs

use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package

eliminiated neg_numeral in favour of - (numeral _)

more tuning for speed

tuning

tuned proofs

killed more needless theorems

killed unused lemmas

optimized more bad apples

optimized 'bad apple' method calls

compile

no need for 3-way split with GFP for a handful of theorems

moved more theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

moved theorems out of LFP

split 'Cardinal_Arithmetic' 3-way

started three-way split of 'HOL-Cardinals'

send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life

merged

show all involved subtyping constraints that cause coercion inference to fail

additional lemmas in BNF/Examples/Stream

reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798

comments by Sean Seefried

more robust example;

tuned proofs;

tuned;

tuned proofs;

explicit indication of thy_load commands;

centralized management of pending buffer edits;

merged

added functions all and exists to IArray

prefer explicit "document" flag -- eliminated stateful Present.no_document;

simplified HTML linefeed (again, see 041dc6d8d344);

simplified HTML theory presentation;

removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;

tuned;

merged

tuned proofs;

tuned signature;

tuned signature -- clarified Proof General legacy;

toplevel function "use" refers to raw ML bootstrap environment;

obsolete;

proper thy_load command 'boogie_file' -- avoid direct access to file-system;

tuned signature;

updated example;

prefer UTF8.decode_permissive;

more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;

more specific Protocol_Output: empty message.body, main content via bytes/text;

tuned imports;

tuned signature;