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

updated sessions;

proper latex -- NB: cannot use antiquotation here;

merged

simplified App template;

obsolete;

obsolete;

tuned message;

tuned signature -- removed obsolete Addsimprocs, Delsimprocs;

tuned signature;

minor doc fix

merged

merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;

removed obsolete RC tags;

Added tag Isabelle2013-1 for changeset 9c1f21365326

tuned;

more on completion;

adjust modules for Admin/build jars_test;

tuned whitespace;

added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);

transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;

Added tag Isabelle2013-1-RC4 for changeset 594628261376

updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);

tuned;

misc tuning;

updated to jedit_build-20131106 (Console.jar 5.1.3);

join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;

tuned signature;

less tiny font for search criteria;

tuned tooltips;

swap equations and premises in the coinductive step for better proof automation

no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;

tuned;

CONTRIBUTORS

more on text completion;

tuned;

more on Monitor panel;

more on Timing;

more on miscellaneous tools;

more screenshots;

more screenshots;

more on Sledgehammer; more on Find;

more on automatically tried tools;

more on prover output; more sections;

misc tuning and clarification;

more on file-system access; provide ISABELLE_HOME_USER as well;

tuned;

more on problems and workarounds;

tuned;

clarified isabelle options -l;

tuned;

clarified workaround: problem is potential blocking of vacuous input (see also Poly/ML SVN 1874);

removed dead code (see also db4bf4fb5492);