proper bib entry;

prevent incoherent default in SideKick 1.7;

corrected path in doc

tuned;

more documentation;

more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);

Added tag Isabelle2015-RC3 for changeset e0c3e11e9bea

tuned;

CONTRIBUTORS

update isar-ref on Lifting

NEWS

tuned;

more on GTK;

more on Isabelle document preparation and bibtex files;

tuned spelling;

updated screenshot;

improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')

made split-rule tactic go beyond constructors with 20 arguments

proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;

tuned output to resemble input syntax more closely;

updated Eisbach, using version fb741500f533 of its Bitbucket repository;

proper header;

tuned output;

tuned output;

tuned output;

tuned output;

tuned output -- avoid empty quites and extra breaks;

tuned;

suppress formal sort-constraints, in accordance to norm_hhf_eqs;

make SML/NJ more happy;

tuned message;

add testing file for code_dt extension of lifting

handle error messages also in after_qed

reorder some steps in the construction to support mutual datatypes

more readable error message if some types do not correspond to sort constraints of the datatype

better precomputing

equivalence in code_dt data structure must respect both rty and qty

don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned

go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype

tuned proof; forget the transfer rule for size_fset

return also which code equation was used; tuned

publish lifting_forget and lifting_udpate interface

note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional

export the result of lifting_def

useful function

parametrize liting of terms by quotients

improve handling of predicators in rsp_thm

tuned; store pred_simps

lift_definition: return the result of lifting

lift_definition: interface also with tactic

generalize prove_schematic_quot_thm

added pred_def, rel_eq_onp tuned

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

updated screenshot;

clarified markup range;

modifier markup for all parsed tokens; report literal token markup, before re-assignment;

updated screenshots;

updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;

avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);

allow sorts on dead variables in BNFs

tuned whitespace;

avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;

code equations as displayable content in code dependency graph

filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified

added checkbox for try0;

made CVC4 support work also without unsat cores

more paranoia settings, e.g. relevant for Ubuntu 15.04;

Added tag Isabelle2015-RC2 for changeset 8483c2883c8c

always traverse required nodes, e.g. relevant for inlined errors of imported theory header;

tuned;

tuned message, in accordance to ML side;

tuned settings to avoid sporadic crashes;

clarified settings for default Poly/ML version: test the actual Isabelle component;

avoid binding warning in Nitpick

doc

clarified permissions;

allow diagnostic proof commands with skip_proofs;

tuned signature;

updated polyml according to fixes-5.5.2 SVN version 2009;

declare Nitpick atoms to avoid '??.' prefixes in output

proper isatest machine;

prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;

this warning is hardly useful but produces noisy markers in the jedit interface

undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)

generalized tends over powr; added DERIV rule for powr

added acknowledgment

general Taylor series expansion with integral remainder

generalized class constraints

generalized differentiable_bound; some further variations of differentiable_bound

moved basic lemmas about has_vector_derivative

closures of intervals

add lfp/gfp rule for nn_integral

strengthened lfp_ordinal_induct; added dual gfp variant

add rules for least/greatest fixed point calculus

rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity

no more simp_legacy_precond

no longer needed

swap False to the right in assumptions to be eliminated at the right end

merged

simplified statement and proof

tuned spelling;

Merge

Merge

Merge

tidying some messy proofs

new simp rule

more formal source, more PIDE markup;

tuned -- avoid odd rebinding of "ctxt" and "context";

tuned;

use smaller example that fits into 64MB string limit of Poly/ML x86 platform;

tuned;

Tidying. Improved simplification for numerals, esp in exponents.

allow sorts on dead variables in BNFs

added known bug

tuning

undid 6d7b7a037e8d

New material about complex transcendental functions (especially Ln, Arg) and polynomials

Fixed a non-terminating proof (almost certainly caused by no change of mind)

new lemma

new ==> simp rule

improved docs

merged

merged

added simp rules for ==>

fixes for limits

New material, mostly about limits. Consolidation.

be less specific about POLYML_HOME, take component setup instead

declare Nitpick atoms to avoid '??.' prefixes in output

back to post-release mode -- after fork point;

acknowledgment

suppressed warnings

updated docs, esp. relating to 'datatype_compat'

typo

clarified keywords for quasi-command spans and Sidekick structure;

merged

tuned;

clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);

tweak afp mac options, try 64bit

compactified proposition

merged

Added tag Isabelle2015-RC1 for changeset c9760373aa0f

tuned spelling;

sorted by automatic regeneration;

updated polyml according to fixes-5.5.2 SVN version 2007;

make SML/NJ happy;

just one line, to make it work with makedist_bundle;

merged

added Eisbach, using version 3752768caa17 of its Bitbucket repository;

merged

rewrite: work purely conversion-based

ANNOUNCE material, based on NEWS;

tuned;

tuned for release;

merged;

finprod takes 1 in case of infinite sets => remove several "finite A" assumptions

(low importance) NEWS

merged

merged

rewrite: add default pattern "in concl" for more cases

more session groups;

allow to exclude session groups;

merged

removed trivial lemmas

proper Theory.check;

make SML/NJ happy;

merged;

clarified document antiquotation: same check as in ML antiquotation;

formal Theory.check, with markup and completion;

tuned;

discontinued pointless warnings: commands are only defined inside a theory context;

tuned comment;

more explicit bootstrap_thy; clarified error;

explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;

clarified thy_deps;

tuned;

tuned signature;

misc tuning and clarification;

let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);

rewrite: use distinct names for unnamed abstractions

avoid mix of languages;

merged

NEWS;

ensure that deps are defined in entries, to prevent crash of Graph_View.build_graph;

updated to jdk-7u80, the latest and last public release of Java 7;

session graph with folded base theories, as in document preparation;

tuned signature;

merged

rewrite: add ML interface

use wasysym for \<hole>;

tuned signature, clarified modules;

tuned messages;

obsolete (see also 94b2690ad494);

GUI controls for ML_statistics, for more digestible protocol dump;

more robust error handling of commands that are declared but not yet defined;

NEWS;

clarified sledgehammer options to approximate old-style diagnostic command;

prepared for more meta-simp rules (by Stefan Berghofer)

merged

add various lemmas about pmfs

lemmas about integrals over bind and join on measures

add lemmas

generalise lemmas; add version of monotone convergence for countable integrals

add lemma about monotone convergence for countable integrals over arbitrary sequences

add lemmas about restrict_space

move lemma from AFP/Coinductive

move some lemmas from AFP/Coinductive

more lemmas about ereal

more lemmas for cset

add lemmas

add lemmas

merged

rewrite: tuned code, no semantic changes

rewrite: with asm pattern, propagate also remaining assumptions to new subgoals

rewrite: do not descend into conclusion of premise with asm pattern

rewrite: with asm pattern, try all premises for rewriting, not only the first

tuned

rewrite: propagate premises to new subgoals

reformat comments

rewr_cconv: ignore premises when tuning conclusion

enable \<hole> syntax for rewrite

call Goal.prove only once for a quadratic number of theorems

predicate compiler: ignore Abs_filter and Rep_filter

merged

moved _aux functions from AFP/Collections to AList

merged

replace Filters in NSA by HOL-Filters

move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

add cofinite filter

add frequently as dual for eventually

add quantifier syntax for eventually

move filters to their own theory

fix latex in Transcendental

proper site for Cygwin setup;

less ambitious collection of quasi-generic PIDE modules;

tuned;

autorebase.bat.done no longer exists in Cygwin 1.7.35 -- lets hope that its incremental rebasing works for us;

merged

tuned -- avoid ML warnings;

avoid redundant shell process;

clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]

tuned;

merged

proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);

tuned whitespace;

Merge

Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

Merge

Merge

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

updated for release;

updated for release;

Added tag Isabelle2015-RC0 for changeset 42d34eeb283c

more uniform Isabelle_System.mkdirs in ML/Scala; avoid odd permission problems on Windows (e.g. Desktop) by using "mkdirs" from Cygwin;

updated for release;

tuned;

tuned spelling;

misc tuning for release;

make SML/NJ more happy;

make SML/NJ more happy;

tuned;

updated Cygwin near 1.7.35-1;

have 'primrec' return definitions

renamed ML funs

generalized code a bit

generalized code

exported function (for symmetry)

merged

renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset

tuned proofs;

tuned signature;

tuned;

renamed misleading option

obsolete;

make SML/NJ more happy;

merged

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

tuned signature

fixed typo in function name

removed a refute example that caused trouble with testing

introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)

merged

conversion between division on nat/int and division in archmedean fields

replace almost_everywhere_zero by Infinite_Set.MOST

option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;

tuned signature;

misc tuning for release;

merged

eliminated suspicious Unicode character;

eliminated hard tabs;

more standard access to goal state;

more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;

added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);

proper test for session HOL-Library;

tuned;

tuned signature;

proper context for Object_Logic operations;

explicitly checked alpha conversion -- actual renaming happens outside kernel;

more standard access to specific subgoal;

tuned wording

updated 'old_smt' to loss of 'z3_non_commercial' option

Z3 news

updated certificates to latest Z3 (and took out one problem that no longer works)

updated docs to reflect actually run ATPs

reorder provers to reflect current eval results

updated docs to Z3 open source

updated SMT module and Sledgehammer to fully open source Z3

updated to new Z3

renamed multiset ordering to free up nice <# etc. symbols for the standard subset

removed TODO

consistent naming

merged

more lemmas and operations on cset (adapted from FSet)

tuned signature;

tuned;

misc tuning for release;

merged

Removed mcard because it is equal to size

generalized slightly

generalized code

generalized code

export ML function

recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;

more qualified names -- eliminated hide_const (open);

tuned;

merged

local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;

support for 'restricted' modifier: only qualified accesses outside the local scope;

tuned;

clarified rail syntax;

@{command_spec} is superseded by @{command_keyword};

clarified command keyword markup;

more position information and PIDE markup for command keywords;

allow prefix before keyword, notably 'private';

support local command setup;

proper header; misc tuning;

tuned signature;

tuned;

new theory Library/Tree_Multiset.thy

more standard local_theory command setup;

some explanation of 'private';

tuned message;

more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

support private scope for individual local theory commands; tuned signature;

rearranged sessions to save approx. 1min elapsed time, 5min CPU time;

obsolete (see 8b7caf447357);

check wrt. proper context, e.g. relevant for 'experiment' target;

clarified name space policy: show less stuff in usual print functions;

unused;

more uniform "verbose" option to print name space;

tuned;

merged

proper treatment of internal method name as already checked Token.src;

tuned signature;

export for informative purposes;

sort constraints are inherent part of class abbreviations (in contrast to class constants)

semidom contains distributive minus, by convention

clarified method_closure; added option for Eisbach, which makes its own closure;

operation on embedded sources for Eisbach;

tuned signature;

tuned -- emphasize semantics of already checked src;

misc tuning -- keep name space more clean;

tuned;

merged

misc tuning -- keep name space more clean;

added command 'experiment';

imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;

NEWS;

clarified "main" group, e.g. relevant for Isabelle/jEdit menu;

evade popular keyword;

tuned signature;

clarified module; more parallel processing;

ISABELLE_JAVA_SYSTEM_OPTIONS for scala REPL;

more reactive interrupts;

added isabelle build option -x, to exclude sessions;

added isabelle build option -k, for fast off-line checking of theory sources;

tuned signature;

tuned message;

tuned signature;

more visibility flags on background naming;

support for explicit scope of private entries;

subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;

tuned signature;

tuned signature;

tuned -- avoid exotic Name_Space.defined_entry;

tuned;

clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;

tuned;

tuned message;

more standard Long_Name operations;

tuned;

tuned;

tuned signature;

simplified code

Theorem "arctan" is no longer a default simprule

John Harrison's example: a 32-bit approximation to pi. SLOW

HOL Light Libraries for complex Arctan, Arcsin, Arccos

arcsin and arccos lemmas

NEWS

given up separate type classes demanding `inverse 0 = 0`

Merge

rationalised and generalised some theorems concerning abs and x^2.

added lemmas

Merge

New material and binomial fix

tuned doc

merged

tuned signature;

support for strictly private name space entries; tuned signature;

tuned signature;

export more low-level theorems in data structure (partly for 'corec')

tuned;

merged

more uniform syntax for named instantiations;

merged

added locale for semirings

exposed approximation in ML

clarified NEWS (cf. 97872c658a44);

clarified equality of formal entities;

merged

tuned signature;

ind_cases: clarified preparation of arguments;

support for minimal specifications, with usual treatment of fixes and dummies;

tuned;

tuned;

tuned signature;

proper local Proof_Context.arity_sorts;

more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;

avoid low-level tsig operations;

tuned;

clarified context;

rule_insts_schematic is considered legacy and false by default;

tuned;

clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain

dropped long-outdated comments

merged

clarified goal context;

clarified goal context;

prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

proper Rule_Insts.read_term, e.g. to enable case_tac using "_";

tuned signature;

clarified goal context;

clarified doc

more graceful failure if some of the involved BNFs have no data

sort BNFs in output

preserve order of type arguments in pre-FP BNF typedef

register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

store low-level (un)fold constants

export more functions

restored broken metis proof

distributivity of partial minus establishes desired properties of dvd in semirings

explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation

modernized

more multiset theorems

semantic completion for @{system_option};

clarified position;

HOL-SPARK .prv files are subject to system option spark_prv; tuned;

tuned signature;

NEWS;

prefer local fixes;

proper signature; tuned;

dummies may depend on goal params as well;

merged

proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

clarified case_tac fixes and context;

clarified name;

option to control old-style schematic mode;

clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;

tuned;

tuned proof;

admit dummy patterns in instantiations; clarified context;

clarified input source;

tuning

reordered properties

NEWS;

tuned proof;

implicit goal parameters are improper;

merged