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

Added tag Isabelle2013-1-RC3 for changeset fbcaa9f08879

avoid non-portable int constant -- make SML/NJ happy;

avoid empty input and its adverse effect on socket communication, e.g. output message getting "stuck" after vacuous update due to Session.update_options;

prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;

basic IO buffer size like for fifo -- imitate implicit flushing behaviour more closely;

removed junk (cf. 409d7f7247f4);

fix a citation

declare Quotient_Examples/FSet.thy as almost obsolete

update documentation of important public ML functions in Lifting

update documentation of Lifting/Transfer and Quotient

don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.

tuned;

more screenshots; tuned;

tuned;

misc tuning;

more strict find_command -- avoid invalid hyperlink_command;

more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;

obsolete;

clarified Editor.current_command: allow outdated snapshot; more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

make double sure that AWT/Swing antialiasing is enabled (see also http://www.jedit.org/users-guide/jvm-options.html and jdk/src/share/classes/sun/awt/SunToolkit.java);

more documentation;

more documentation;

more documentation;

tuned;

NEWS;

avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);

add congruence rule to prevent code_simp from looping

Added tag Isabelle2013-1-RC2 for changeset 782e430e6a83

native executable for Linux (see Admin/Linux);