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