clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context; tuned;

clarified context;

clarified context;

proper context;

tuned;

clarified context;

updated to scala-2.11.6;

Thm.cterm_of and Thm.ctyp_of operate on local context;

merged

merged

clarified context;

tuned -- more explicit use of context;

tuned -- more explicit use of context;

A few new lemmas and a bit of tidying up

Merge

The function frac. Various lemmas about limits, series, the exp function, etc.

avoid needless 'if ... undefined' in generated theorems

strengthened tactic

strengthened tactic

deal better with corecursion through functions

removed too strict checks

message tuning

tuning

improved primcorec messages

improved primcorec messages

better primcorec messages

more primcorec messages

more precise primcorec messages

more precise primcorec messages

better primcorec messages

more 'primcorec' error handling

helpful error message when 'auto' fails

no quick_and_dirty for goals that may fail + tuned messages

tuned new primrec messages

reworked primcorec error messages

fix import path

merged

tuned signature;

tuned signature;

removed unused; tuned comments;

merged

Removed the obsolete functions "natfloor" and "natceiling"

clarified signature;

tuned;

tuned;

merged;

tuned signature -- prefer qualified names;

alist is a BNF

eliminated some clones of Proof_Context.cterm_of

updated docs

strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"

SPASS-Pirate is now called Pirate

avoid duplicate simp warning for datatypes with explicit products

removed needless (and inconsistent) qualifier that messes up with Mirabelle

import 'Main' to be on the safe side

added Proof_Context.cterm_of/ctyp_of convenience;

tuned;

updated to jedit-5.2.0; updated CommonControls.jar, kappalayout.jar, MacOSX.jar, SideKick.jar;

spelling

tuned whitespace;

typo

tuned;

updated CVC4 component to include libgmp on Mac OS X

more uniform headless mode for all derivatives of "build" (amending df5dc24ca712);

Goal.prove_multi is superseded by the fully general Goal.prove_common;

proper LaTeX;

make SML/NJ more happy;

added new tree material

generalised the results by Eberl

more canonical order of subscriptions avoids superfluous facts

got rid of linordered_field_class.sign_simps(41) !

establish unique preferred fact names

eliminated technical fact alias

eliminated fact duplicates

inlined rules to free user-space from technical names

explicit declaration allows cumulative declaration

use more permissive logic for CVC4 (in case both reals and datatypes appear)

deleted ineffective declarations

dropped unused rules

more direct expression of syntactic function records

self-contained declaration attribute

simpset with no redundancy

times_divide_eq rules are already [simp] despite of comment

explicit equivalence for strict order on lattices

tuned

purge variables not mentioned in body from pattern

only collapse patterns with disjunctive variable names

clarified

avoid unused arguments

tuned

more consistent teminology

fact consolidation

dropped redundancy

less warnings

merged

proper context; tuned;

proper context; eliminated clone;

proper context;

proper context; tuned whitespace;

proper context and method setup;

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;