merged

more uniform command setup;

added 'paragraph', 'subparagraph';

clarified Latex.environment;

more explicit output of list items;

tuned;

clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;

Markdown support in document text;

clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;

clarified modules;

load markdown.ML into Pure;

proper recursive nesting of adjacent lists;

tuned;

clarified line content: source without marker prefix;

more markup;

report Markdown document structure;

more comments;

unused -- avoid confusion in Symbols dockable;

proper nesting of adjacent lists;

more document structure; tuned signature;

more document structure;

more document structure;

clarified;

minimal support for Markdown documents;

clarified;

more symbols;

more symbols;

clarified control symbols;

added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;

tuned signature (cf. XML.trim_blanks);

added split_lines; tuned signature;

qualify some names stemming from internal bootstrap constructions

removed too aggressive underscorization

typo

prefer undecorated typedef

even -> evn to avoid clash with global even

added invar empty

Fixed nonterminating "blast" proof

new material on path_component_sets, inside, outside, etc. And more default simprules

restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment

prod_case as canonical name for product type eliminator

emphasized general nature of parameter

moved lemmas

more symbols;

redundant due to \parindent 0pt;

isabelle update_cartouches;

scalable fonts for T1 encoding;

proper imports; more symbols; avoid special latex tricks;

more symbols;

more symbols;

more antiquotations;

proper message;

clarified antiquotation;

spelling;

unused;

obsolete;

@{verbatim [display]} supersedes old alltt/ttbox;

@{verbatim [display]} supersedes old alltt/ttbox;

more symbols;

some control symbols for markup and formatting;

allow control symbols within markup body;

added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;

proper document source;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- less symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned syntax -- more symbols;

tuned whitespace;

tuned;

tuned syntax -- more symbols;

more symbols;

more symbols;

more symbols;

prefer symbols;

use Isabelle symbols by default;

isabelle update_cartouches;

more explicit HTML.symbols; tuned signature;

NEWS;

more direct HTML presentation, without print mode;

discontinued specific HTML syntax;

installable TTF for MS IE 9+;

output HTML text according to Isabelle/Scala Symbol.Interpretation;

tuned output;

server-side fonts;

more accurate imitation of "cp -p -f";

more Present operations on Scala side;

clarified, according to Isabelle_System.copy_file in ML;

NEWS

documentation for transfer debug methods

add a file with examples of debugging transfer

new methods for debugging transfer and transfer_prover

right parenthesization

made TPTP SZS status more compliant

tuning

measurable sets on product spaces are embeddings of countable products

generalize eqI theorems for product measures

isabelle update_cartouches;

more glyphs from DejaVuSansMono and DejaVuSansMono-Bold: 0100-017F Latin Extended-A, 0180-024F Latin Extended-B;

cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution

avoid 'legacy binding' warning

removed dead code

merged

back to old-fashioned GC, which appears to work better with interactive applications;

routine check of theory context;

proper context;

proper context;

clarify docs

updated docs

made documentation more accurate

disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier

avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations

parallel tests: 6h & 12h;

news

generate 'case_transfer' unconditionally

isabelle update_cartouches;

isabelle update_cartouches;

merged

avoid hardwired frees; tuned;

added Thm.forall_intr_name;

added 'proposition' command;

fewer aliases for toplevel theorem statements;

just one theorem kind, which is legacy anyway;

pretty_const: proper local name space; tuned;

collect the names from goals in favor of fragile exports

compile

tuning

avoid legacy syntax

further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes

added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs

merged

tuned signature;

produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;

avoid too aggressive optimization of 'finite' predicate

avoid unsound simplification of (C (s x)) when s is a selector but not C's

extended theory exporter to also export MePo-selected facts

speed up MaSh duplicate check

sped up MaSh nickname generation

merged

more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;

speed up MaSh

updated docs and NEWS

updated docs

removed Nitpick nonblocking mode, that was never really used

adapted example

removed obsolete material in documentation

further reduced dependency on legacy async thread manager

removed legacy asynchronous mode in Sledgehammer

better compliance with TPTP SZS standard

merged

avoid useless empty case_names;

clarified init (again): isabelle.Main is responsible to provide basic JVM setup, jedit.jar picks this up (e.g. list of known fonts), plugin cannot be loaded in isolation without isabelle.Main;

New theorems about connected sets. And pairwise moved to Set.thy.

less ambitious regex -- avoid unclarities of escaping;

tuned documentation

tuned datatype docs

export proof method in signature

export '_cmd' functions

back to old JavaAppLauncher to avoid initial startup problems (due to unsigned application?);

tuned GUI;

proper isabelle.root for bootstrap;

merged

tuned;

proper Cygwin.init (amending e00e1bf23d03);

renamed jvmpath to platform_path;

clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);

tuned GUI;

uniform treatment of bootstrap directories; Isabelle_System.init() includes Cygwin.init(), e.g. for situations without isabelle.Main; tuned;

more robust system init (again), in case the plugin is started without isabelle.Main;

tuned message;

clarified modules; more conventional GUI threading;

Merge

Dead wood removal

Merge

real_of_nat_Suc is now a simprule

updated docs

clarified Isabelle_System.init; clarified GUI.init_laf; clarified modules; tuned signature;

tuned;

tuned GUI;

proper event;

tuned GUI;

build session within running jEdit;

clarified modules;

monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime

more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

Caratheodory: cleanup and modernisation

restructure fresh variable generation to make exports more wellformed

more canonical context threading

merged

documentation for "Semantic subtype definitions"; misc tuning and simplification;

moved remaining display.ML to more_thm.ML;

less redundant output;

proper context;

tuned;

tuned;

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