tuned;

tuned signature: eliminated pointless type Context.pretty;

more explicit Defs.context: use proper name spaces as far as possible;

explicit indication of overloaded typedefs;

tuned signature;

tuned output;

tuned output;

tuned signature;

eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;

tuned signature;

tuned output;

separate command 'print_definitions';

tuned;

clarified deps entry: global names for arguments;

renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;

tuned signature;

tuned whitespace;

HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;

prove Liminf_inverse_ereal

merged

exchange uniform limit and integral

congruence rules for the relator

conceal only the definitional theorems of map, set, rel (and not the actual constants)

more useful properties of the relators

tuned proofs (less warnings)

Useful facts about min/max, etc.

Merge

fixed a VERY SLOW proof

SOME rather than THE makes it easy to prove equivalence with other forms of derivatives

New lemmas

Prepared two non-terminating proofs; no obvious link with my changes

added AVL and lookup function

tuned

merged

unified isin-proofs

tuned

include some data structures into code generation

effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level

tuned references

added red black trees

clarified markup; tuned signature;

isabelle update_cartouches;

merged

tuned GUI;

removed auto update -- bad reactivity;

clarified isabelle.update-state;

more reactive update, like Output panel;

added isabelle update_then;

NEWS;

tuned priority (like other query operations, e.g. "find_theorems");

option editor_output_state;

obsolete, superseded by State panel;

added action "isabelle-update-state"; tuned signature;

support for auto update via caret focus;

tuned signature;

separate panel for proof state output;

tuned;

more specific name to reduce danger of clash with direct uses of plain Command.print_function;

tuned;

new lemmas and movement of lemmas into place

New subdirectory for functional data structures

Added new simplifier predicate ASSUMPTION

eliminated suspicious unicode;

eliminated hard tabs;

obsolete;

NEWS;

straight-forward refresh, without special preconditions; eliminated somewhat expensive eq_content;

eliminated pointless jedit_text_overview_limit;

fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;

allow to cancel running event; synchronized postpone operation;

tuned;

tuned signature;

Merge

Massive revisions, as a valid path must now be continously differentiable (C!)

isabelle update_cartouches; tuned proofs; tuned whitespace;

isabelle update_cartouches;

recode all text, which is relevant for Session.save on non-ASCII directory;

tuned;

more recent JavaAppLauncher, which supports file associations;

more explicit indication of bundled jdk, which is required for newer versions of JavaAppLauncher;

more app properties glimpsed from infinitekind/Moneydance 2015.5;

tuned whitespace;

updated to polyml-5.5.3-20150916 (polyml git version cb1b36caa242);

avoid module dependency cycles

goali -> i

Omega_Words_Fun: Infinite words as functions from nat.

provide FontMapper for embedded fonts;

avoid hardwired colors; more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);

avoid hardwired colors;

replacement character for spaces;

single-instance application, even on Linux;

single-instance application for Linux;

tuned message;

added isabelle jedit_client;

tuned proofs -- less legacy;

tuned message;

tuned proofs;

renamed method "goals" to "goal_cases" to emphasize its meaning;

tuned proofs;

method "goals" ignores facts;

tuned;

unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification; also unconceal corresponding primitive definitions, which are official conversions between predicates and sets

fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;

single-instance application on Windows;

more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;

convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;

clarified order;

more symbols;

Unicode is standard in Poly/ML repository version;

removed obsolete undocumented feature;

more standard local_theory operations; eliminated slightly odd @{cpat};

HOL-Proofs is slow;

convenient access to application properties;

tuned -- avoid slightly odd @{cpat};

dropped redundant NEWS

less ambitious options, to accomodate 4GB systems;

tuned

clarified declaration flags, like 'declaration' command;

merged

simplified simproc programming interfaces;