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;

immutable byte vectors versus UTF8 strings;

dropped duplicate of of_bool

proper code equations for Gcd and Lcm on nat and int

tuned

fixed type variable confusion in 'datatype_new_compat'

implemented 'tptp_translate'

reintroduced (unimplemented) 'tptp_translate' tool

have MaSh support nameless facts (i.e. proofs) and use that support

made SML/NJ happy

renamed thm

explicit inclusion of data refinement theory into HOL-Library session

tuned to improve automation (for REPEAT)

separated comparision on bit operations into separate theory

prohibit locally fixed type variables in bnf definitions

tuned

standard relator for list bnf

tuned example

shortened generated property name

more explicit syntax for defining a bnf

fix document generation for HOL-Probability

fix document generation for Extended_Nat

measure of a countable union

add restrict_space measure

better support for enat and ereal conversions

enat is countable

add equalities for SUP and INF over constant functions

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

add acyclicI_order

stronger inc_induct and dec_induct

countability of the image of a reflexive transitive closure

support of_rat with 0 or 1 on order relations

equation when indicator function equals 0 or 1

ported part of function package to new 'Ctr_Sugar' abstraction

undid copy-paste

ported 'partial_function' to 'Ctr_Sugar' abstraction

port list comprehension simproc to 'Ctr_Sugar' abstraction

added convenience function

document idiomatic use of 'simps_of_case'

ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

register old-style datatypes as 'Ctr_Sugar'

export useful ML function

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

tuned headers

moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction