Series.thy is based on Limits.thy and not Deriv.thy

move Ln.thy and Log.thy to Transcendental.thy

move SEQ.thy and Lim.thy to Limits.thy

HOL-NSA should only import Complex_Main

rename RealVector.thy to Real_Vector_Spaces.thy

rename RealDef to Real

remove Real.thy

merge RComplete into RealDef

move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

remove posreal_complete

separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef

Discontinued theories src/HOL/Algebra/abstract and .../poly.

Remove obsolete URLs in documentation of HOL-Algebra.

Fix issue related to mixins in roundup. Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.

simp_const -> afold; bfold -> fold'; bsimp_const -> bfold

added lemmas

merged

clarified text_fold vs. fbrk;

tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;

tuned message;

actually exit on scalac failure;

tuned signature;

removed obsolete uses of ext

prefer preset = 3 -- much faster and less memory requirement;

basic support for xz files;

added component xz-java-1.2;

more "quick start" hints; more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle"; tuned;

simple case syntax for stream (stolen from AFP/Coinductive)

prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); tuned proofs;

merged

reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;

apply small result immediately, to avoid visible delay of text update after window move;

structural equality for Command.Results; more general Command.State.eq_content;

allow fractional pretty margin -- avoid premature rounding;

more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

tuned;

spelling

fundamental revision of big operators on sets

tuned proof

locales for abstract orders

merged

added rudimentary induction rule for partial_function (heap)

allow induction predicates with arbitrary arity (not just binary)

modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0

arcsin and arccos are continuous on {0 .. 1} (including the endpoints)

move continuous_on_inv to HOL image (simplifies isCont_inverse_function)

move connected to HOL image; used to show intermediate value theorem

move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets

move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)

clean up lemma_nest_unique and renamed to nested_sequence_unique

simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano

introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

move first_countable_topology to the HOL image

move metric_space to its own theory

move topological_space to its own theory

proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;

eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;

proofs depend only on constraints, not on def of L WHILE

use the right role for SPASS hypotheses

soundness statement as in type system

add label for referencing in semantics book

tuned

get rid of xcolor warnings

extended stream library

export datatype definition which gets expanded too much in antiquotation

tuned

add induction rule for partial_function (tailrec)

prefer ownerless window, to avoid question of potentially changing parent view;

proper parent component for window.init;

lemma names and a corollary

managed to eliminate further snippets

fewer IMP snippets

merged

extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;

recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;

re-init last window without flipping its visible/disposed state, to avoid odd focus inversion problems;

explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);

tuned

eliminate duplicated constant (diag vs. Id_on)

hide internal constants; tuned proofs

tuned

tuned

added advanced rule induction subsection

merged

more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;

some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;

more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible); more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors); early initialization of gutter to get proper text area painter size (see also 2585c81d840a);

drop a workaround because of 8739f8abbecb

fixing transfer tactic - unfold fully identity relation by using relator_eq

tuned (in particular bold fonts)

merged

document ISABELLE_POLYML;

tuned

simplified time_CPU and time_GC; derive relative speed from time (considered as step function);

updated to scala-2.10.1;

extended stream library (sdrop_while)

tuned signature;

more robust Par_Exn.make, especially relevant for SML/NJ trying to use Par_Exn.release_all;

proper use of "member", without embarking on delicate questions about SML equality types;

made SML/NJ happy;

tuned

merged

clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;

proper formatting, to facilitate line-based diff;

more uniform session descriptions, which show up in chapter index;

proper index for HOL-Proofs, which is also in chapter "HOL";

include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;

more accurate handling of global browser info at the very end (without races), subject to no_build and info.browser_info;

sessions may be organized via 'chapter' in ROOT;

do not absorb I/O errors;

show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;

new lemma subset_decode_imp_le

merged

more IMP snippets

rename fset_member to fmember and prove parametricity

BNF uses fset defined via Lifting/Transfer rather than Quotient

nitpick setup and code generation for streams

merged

tuned

proper path -- I/O was hidden due to permissiveness;

merged

removed odd cvs artifacts;

refurbished some old README.html files as session descriptions, which show up in chapter index;

include session description in chapter index; prefer alphabetical order;

tuned;

more accurate theory links;

discontinued "isabelle usedir" option -r (reset session path); simplified internal session identification: chapter / name; clarified chapter index (of sessions) vs. session index (of theories); discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser); removed obsolete session parent_path;

discontinued "isabelle usedir" option -P (remote path);

support for 'chapter' specifications within session ROOT;

added latex markup

merged

more snippets

added pairs

extended set comprehension notation with {pttrn : A . P}

tuned

more factorisation of Step & Co

factored out Step

merged

stepwise instantiation is more modular

generalized subclass relation; tuned proof

termination proof for narrowing: fewer assumptions

accomodate encrypted file-system on linux;

tuned;

discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types

updated keywords (cf. 84d01fd733cf);

proper type inference for default values

convert mappings to parametric lifting

setup_lifting doesn't support a type variable as a raw type

add [relator_mono] and [relator_distr] rules

simplify Lift_FSet because we have parametricity in Lifting now

patch Isabelle ditribution to conform to changes regarding the parametricity

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

merged

simplified basic termination proof

some simp rules for fset

avoid -Infinity which confuses JFreeChart histogram;

tuned proofs -- more structure, less warnings;

tuned signature -- prefer terminology of Scala and Axiom;

better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)

avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)

netlimit is abbreviation for Lim

tuned proofs

changed has_derivative_intros into a named theorems collection

changed continuous_on_intros into a named theorems collection

changed continuous_intros into a named theorems collection

add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->

major redesign: order instead of preorder, new definition of intervals as quotients

added lemma

extended numerals

merged

merged

removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);

extended stream library a little more

extended stream library

generalized lemmas in Extended_Real_Limits

eventually nhds represented using sequentially

generalized compact_Times to topological_space

move lemma Inf to usage point

tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)

tuned proofs (used continuity of infdist, dist and continuous_attains_sup)

generalized continuous/compact_attains_inf/sup from real to linorder_topology

continuity of pair operations

use generate_topology for second countable topologies, does not require intersection stable basis

generalized isGlb_unique

complete_linorder is also a complete_distrib_lattice

move Liminf / Limsup lemmas on complete_lattices to its own file

merged

New theory of infinity-extended types; should replace Extended_xyz eventually

Avoid ML warning about unreferenced identifier.

polymorphic SPASS is also SPASS

allow more general coercion maps; tuned;

more lemmas about intervals

merged

refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;

join all proofs before scheduling present phase (ordered according to weight); tuned;

more explicit datatype result;

split dense into inner_dense_order and no_top/no_bot

move auxiliary lemmas from Library/Extended_Reals to HOL image

tuned (extend datatype to inline option)

prefer more systematic Future.flat;

more uniform Future.map: always internalize failure; added Future.flat as fast-path operation;

uniform treatment of global/local proofs; tuned;

tuned;

clarified Toplevel.element_result wrt. Toplevel.is_ignored;

more Thy_Syntax.element operations;

coercion-invariant arguments at work

constants with coercion-invariant arguments (possibility to disable/reenable coercions under certain constants, necessary for the forthcoming logically unspecified control structures for case translations)

simplified Proof.future_proof;

provide explicit dummy names (cf. dfe469293eb4);

discontinued empty name bindings in 'axiomatization';

provide common HOLogic.conj_conv and HOLogic.eq_conv;

just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;

discontinued obsolete 'axioms' command;

more robust build error handling, e.g. missing outer syntax commands;

eliminated legacy 'axioms';

eliminated legacy 'axioms';

eliminated legacy 'axioms';

eliminated legacy 'axioms';

eliminated legacy 'axioms';

eliminated legacy 'axioms';

eliminated legacy 'axioms';

marginalized historic strip_tac;

tuned proof;

tuned whitespace and indentation;

simplified imports;

load timings in parallel for improved performance;

proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);

parallel dep.load_files saves approx. 1s on 4 cores;

eliminated pointless re-ified errors;

merged

discontinued redundant 'use' command;

discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;

discontinued obsolete 'uses' within theory header;

use lemma from Big_Operators

add inclusion/exclusion lemma

added lemma

merged