separate channel for debugger output; clarified thread name;

clarified thread name;

add coinduction rule for infinite

merged

clarified context;

more explicit context; tuned signature;

eliminated dead code;

clarified Variable.gen_all; simplified Local_Defs.export: pointless partial application;

more explicit context;

more direct access to atomic cterms;

clarified context;

proper context;

more direct access to atomic cterms;

clarified context;

clarified context;

clarified context;

merged

merged

added theory Uniform_Limit

evade timeout problem on macbroy6 (potentially due to NFS oddities);

tweaks. Got rid of a really slow step

the Cauchy integral theorem and related material

depth -> height; removed del_rightmost (too specifi)

tuned;

merged

tuned signature; clarified context;

formal class for factorial (semi)rings

merged

NEWS;

tuned signature;

New material for Cauchy's integral theorem

tuned signature for print_nested_cases;

more explicit checks -- improved errors;

eliminated cterm_instantiate;

updated to infer_instantiate; clarified context;

tuned signature;

added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;

eliminated atac, rtac, etac, dtac, ftac;

updated to infer_instantiate;

updated to infer_instantiate;

updated to infer_instantiate;

proper context;

updated to infer_instantiate;

updated to infer_instantiate; clarified context;

ignore non-existant variables, like other instantiate rules;

updated to infer_instantiate;

updated to infer_instantiate;

added infer_instantiate'; clarified boundary cases of instantiate';

more uniform exceptions, like cterm_instantiate;

updated to infer_instantiate; tuned;

more accurate maxidx;

clarified error;

added infer_instantiate, which is meant to supersede cterm_instantiate;

eliminated alias;

proper context;

unused;

proper context;

more symbols by default, without xsymbols mode;

Measures form a CCPO

reorganized Extended_Real

isabelle update_cartouches;

tuned proofs;

proper latex;

tuned proofs;

tuned proofs;

support for ML debugger;

more explicit thread identification;

avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes;

new material for multivariate analysis, etc.

proper LaTeX;

updated to jdk-8u51;

more symbols;

isabelle update_cartouches;

prefer tactics with explicit context;

prefer tactics with explicit context;

merged

prefer tactics with explicit context;

tuned whitespace;

prefer tactics with explicit context;

reactivated dead code;

more uniform ComponentAdapter;

skeleton for interactive debugger;

tuned;

tuned;

store breakpoints within ML environment;

clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default; tuned;

report possible breakpoint positions;

proper attribute;

forgotten selector

made code less loopy

keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)

generalized generic translation function

merge

tuning

generalized limitation in documentation

made tactic more robust w.r.t. equations containing 'case_prod'

merged

merged

clarified boundary cases of completion;

additional ML parse tree components for Poly/ML 5.5.3, or later; support for ML completion; tuned;

added option ML_debugger;

ML debugger interface;

{r,e,d,f}tac with proper context in BNF

move disjoint sets to their own theory

back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);

merged

more explicit command-line option for isabelle build;

more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);

normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;

generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal

add continuous_onI_mono

tuned description

tuning

updated Isabelle description to CASC

imported patch up_casc

add emeasure_add_AE

stronger induction assumption in lfp_transfer and emeasure_lfp

refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h; tuned parameters;

Quickcheck setup for finite sets

tuned proofs;

tuned proofs;

merged

tuned proofs;

SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);

clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);

tuned whitespace;

tuned ML signature (and rationalized code a bit)

merged

case_of_simps: do not split for types with a single constructor

tests for Simps_Case_Conv

merged

clarified context; eliminated dead code;

tuned proofs;

clarified context;

clarified context;

Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;

clarified text folds: proof ... qed counts as extra block;

more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;

tuned;

tuned according to a81dc82ecba3;

tuned facts

more cautious use of [iff] declarations

avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead

eliminated some duplication

more algebraic properties for gcd/lcm

moved normalization and unit_factor into Main HOL corpus

more generous timeout for the sake of HOL-Proofs in at64-poly;

tuned ML signature

have the installed termination prover take a 'quiet' flag

add monotonicity rule for rtranclp

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

tuned proofs;

tuned whitespace;

clarified sections;

clarified sections;

tuned;

clarified sections;

tuned;

tuned;

tuned proofs;

plain string output, without funny control chars;

tuned message;

tuned;

proper outer syntax category, e.g. relevant for PIDE markup;

merged

tuned;

tuned;

clarified sections; tuned whitespace;

clarified section references; tuned whitespace;

tuned;

clarified sections;

removed outdated and mostly obsolete material;

tuned;

tuned whitespace;

clarified context;

obsolete;

clarified context;

clarified context;

more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;

clarified context;

clarified context;

clarified context;

eliminated spurious warning/tracing messages -- avoid Display.string_of_thm_without_context;

clarified context;

clarified context;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

tuned signature;

clarified context;