split into subgoals

tuning

merged

support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;

Removed the infix operator "choose" to allow HOLCF to build

sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex

eliminated unused arith "verbose" flag -- tools that need options can use the context;

eliminated dead code (cf. 5e5c36b051af);

tuned;

clarified aliases;

misc tuning and simplification;

tuned;

misc tuning and simplification;

tuned;

cartouche_declaration for Eisbach;

NEWS;

clarified Drule.gen_all: observe context more carefully;

added declare_maxidx operations for Eisbach;

clarified Variable.export: observe maxidx of target context;

tuned;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

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