new lemmas re refinement of one equivalence relation WRT another

rel_pmf preserves orders

generalise lemma

more lemmas

merged

more transfer rules

add lemmas about functions on option

tuned proof

add lema about card and vimage

add more general version of finite_vimageD

add lemma

add lemmas about flat_ord

add parametricity rules for monotone, fun_lub, and fun_ord

add parametricity rule for Ex1

add intro and elim rules for right_total

add monotonicity lemmas for rel_fun

add lemmas about bind and image

updated NEWS

updated Sledgehammer docs

added CVC4 component (and took out CVC3 from main components)

tuned default provers

Merge

Not a simprule, as it complicates proofs

Merge

New lemmas and a bit of tidying up.

check unused theory;

tuned;

more accurate context; make SML/NJ happy;

merged

misc tuning;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;

indicate slow proof (approx. 20s);

merged

add bind_cond_pmf_cancel

add cond_map_pmf

introduce discrete conditional probabilities, use it to simplify bnf proof of pmf

tuned proof

add another lemma to split nn_integral over product count_space

tune proof

nn_integral can be split over arbitrary product count_spaces

add stronger version of lemma

default abstypes and default abstract equations make technical (no_code) annotation superfluous

careful about visibility of facts that have the same 'theory' in optimization

non-intrusive default code setup for mappings

slightly more standard code setup for String.literal, with explicit special case in predicate compiler

explicit type annotation avoids problems with Haskell type inference

more explicit hint on import order

dropped dead code; tuned

dropped obsolete external entrance point

explicit error message for non-existing targets

fixed typos

less confusing constant

tuning

simp rules for return_pmf

related permutations with bij functions

canonical name

discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;

more explicit indication of Async_Manager_Legacy as Proof General legacy;

tuned bootstrap;

tuned;

explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;

unused;

ensure that running into older execution is interruptible (see also b91dc7ab3464);

clarified worker_wait; clarified join_next/join_loop, with proper thread attributes to allow interrupting of join (e.g. via Lazy.force);

explicit headless mode for machines that lack X11 (e.g. lxbroy10);

more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);

tuned signature;

tuned comment;

tuned signature;

clarified module name;

abstract code equation may also be default

proper term_of for iarray

string printing conformant to both (S)ML and Isabelle/ML

Fixed bug in bugfix for function package

Fixed variable naming bug in function package

moved bcontfun from AFP/Ordinary_Differential_Equations

ereal: tuned proofs concerning continuity and suprema

spelling error

NEWS;

removed unused operations;

prefer plain session_graph.pdf over GraphBrowser applet;

complete pattern coverage, e.g. relevant for singleton graph;

discontinued obsolete option "document_graph";

provide session_graph.pdf via Isabelle/Scala;

support for session graph from Scala side;

support for off-line graph output, without GUI thread;

make it independent from GUI thread, e.g. for Graph_File.write;

separate module Graph_File;

tuned comments;

tuned;

more compact message;

proper naming convention;

prefer plain tuples;

tuned message;

tuned;

tuned signature;

tuned;

tuned message;

more direct Output.output; avoid newline in Code_Printer/Pretty.str;

avoid newline in Pretty.str;

merged

generalise lemma

integral of the product of count spaces equals the integral of the count space of the product type

import general thms from Density_Compiler

backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;

backed out obsolete workaround from ef1edfb36af7

disjunctive bottom and supremum lists

sufficent to have graphview as part of jEdit rather than Pure

option for formally inlined class specifications in hierarchy graph

clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;

updated to jdk-7u76, which appears to be more stable than jdk-8u31 (e.g. crashes jEdit/Console plugin of Mac OS X);

updated jdk-8u31;

generalized sum_diff_distrib to setsum_subtractf_nat

tuned measurability proofs

typo in description

tuned message;

always swap panels, which leads to slightly better GUI layout;

suppress inactive controls (again);

tuned colors;

tuned;

more symmetric layout of main panel; misc tuning;

clarified edge_color;

proper tooltips -- override action toolTip which is empty here;

no document here;

discontinued attempt at alphabetic_order -- selection via regex should be sufficient;

suppress some controls that don't work yet;

proper selection of nodes via regular expression;

obsolete -- full layout takes approx. 100ms;

suppress some controls that don't work yet;

tuned;

misc tuning;

proper scrolling wrt. transform; tuned signature;

clarified main actions and keyboard focus;

tuned signature;

retain uniform background, notably wrt. PDF output and tree panel;

option graphview_swap_panels;

support for tree view on graph nodes; misc tuning;

tuned;

no censorship of L&F;

prefer fractional font metrics, for proper scaling of node size;

tuned metrics;

tuned window size for the sake of Windows L&F;

proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;

more compact content for tighter graph layout;

more explicit Layout.Info: size and content; allow multi-line vertex label, based on content; misc tuning;

clarified Class.pretty_specification: imitate input source;

merged

more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT

added simp lemma

tuned

separate image for prerequisites of codegen tutorial

modernized cartouches

even more pervasive replacement of auxiliary destination

merged

more detailed runtime statistics for Z3 proof reconstruction

merged

proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);

updated to scala-2.11.5;

refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;

more informative build_theories_result: cumulative Runtime.exn_message;

tuned;

more type-safe handler interface; proper progress for Build.Handler;

clarified build_theories: proper protocol handler;

added Promise.cancel;

clarified build_theories;

added Path.decode in ML, in correspondence to Path.encode in Scala;

some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;

piecewise measurability using restrict_space; cleanup Borel_Space

tuned

indent broken lines of bindings in do blocks

more line breaks in integral notation

allow line breaks in integral notation

allow line breaks in probability syntax

don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it

NEWS

measurability prover: removed app splitting, replaced by more powerful destruction rules

tuned warnings: observe Context_Position.is_visible;

removed unused/non-portable with_tmp_fifo;

discontinued fifo channel, always use portable socket;

tuned -- more Sidekick-friendly layout;

do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

more explicit errors;

proper latex;

tuned -- less redundant;

proper Session.save with shutdown, which is relevant to avoid persistent threads;

tuned latex;

merged

always use socket to test performance and stability;

explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

tuned;

discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;

tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;

clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

ignore print process even after fork, to avoid loosing active worker threads;

rel_pmf OO: conversion to nat is not necessary

merged

simplify construction for distribution of rel_pmf over op OO

prefer option for default code printing width

modernized and more uniform style

tuned order

tuned

avoid technical term "mixin" in user documentation text

tuned;

merged

updated bibtex

tuned;

misc tuning;

made SML/NJ happier

configurable options;

proper level distance according to number of edges, as in old browser;

clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;

tuned;

merged

NEWS;

rubberband method as in old browser; tuned;

tuned;

tuned signature;

proper translate vertex (cf. 4d985afc0565);

tuned signature;

explict layout graph structure, with dummies and coordinates; explicit metrics for dummy box; tuned signature; misc tuning;

tuned;

docs

docs

docs

tuning

formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML

merged

clarified visualizer parameters; do not show dummies by default;

tuned metrics;

proper bounding box including dummies;

more direct coordinates for dummy;

separate module Metrics; maintain static metrics (with font) and visible_graph via layout;

tuned imports;