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;

tuned signature;

generalized sup_continuty of add, ereal_of_enat

add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer

moved to lxbroy3, hoping that it works better;

separate (semi)ring with normalization

merged

more CONTRIBUTORS;

documentation for 'subgoal' command;

clarified module;

allow to specify suffix of goal parameters;

subgoal parameters are internal by default and named by user;

split multi-goals as usual (outermost Pure.conjunction only);

clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;

proper state after qed;

clarified keyword categories;

support for subgoal focus command;

tuned;

taylor series with has_integral and integrable_on

merged

no arguments for "standard" (or old "default") methods;

renamed "default" to "standard", to make semantically clear what it is;

tuned;

Merge

Useful lemmas. The theorem concerning swapping the variables in a double integral.

generalized inf and sup_continuous; added intro rules

fix tex-output for rel_mset

removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs

clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c); apply_end cases are no longer seen in current context section (hardly relevant in practice);

improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);

clarified static phase; proper error;

tuned proofs;

more symbols;

more symbols; tuned proofs; tuned ML;

corrected typo

tuned src/HOL/ex/Ballot

add examples from Freek's top 100 theorems (thms 30, 73, 77)

generalized geometric distribution

added lemma

simplified termination criterion for euclidean algorithm (again)

tuned proof

rings follow immediately their corresponding semirings

tuned code setup

algebraic specification for set gcd

premises in 'show' are treated like 'assume';

adapted to a9b71c82647b;

merged

isabelle update_cartouches;

more symbols; eliminated alternative syntax;

tuned proofs;

do not expose goal parameters;

more symbols;

more symbols;

proper spacing, as for other syntax for these symbols;

tuned whitespace;

updated SystemOnTPTP URL

tuned proofs;

merged

implicit goal cases are legacy;

tuned proofs;

more heap -- hoping for more stability of HOL-Proofs;

added method "goals" for proper subgoal cases;

tuned signature;

tuned signature;

tuned;

tuned;

tuned signature;

streamlined definitions and primitive lemma of euclidean algorithm, including code generation

euclidean algorithm on polynomials

more theorems

generalized to definition from literature, which covers also polynomials

put E before (typically remote, hence less reliable) Vampire

tuned proofs -- less digits;

updated to scala-2.11.7;

clarified 'case' command;

silence 'try'

Merge

Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.

tuned proofs;

tuned proofs;

merged

tuned proofs;

tuned proofs;

tuned;

support 'when' statement, which corresponds to 'presume';

added method "sleep";

tuned signature;

tuned whitespace;

clarified nesting of Isar goal structure; tuned message;

tuned;

keep 'Pure.all' in goals when preplaying

use right context for preplay, to avoid errors in fact lookup

reverted some too aggressive TPTP interpreter changes

automatically build image

filter out more Poly/ML messages from (ad hoc) TPTP toools

removed (now illegal) semicolons in generated theory files

use CVC4 instead of CVC3 at CASC

fixed typo

modernized name

more symbols;

tuned proofs;

tuned proofs;

eliminated list_all;

tuned proofs;

tuned proofs;

tuned proofs;

isabelle update_cartouches;

misc tuning;

less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home;

isabelle update_cartouches;

avoid suspicious Unicode;

tuned;

tuned proofs;

isabelle update_cartouches;

merged

removed dead code;

discontinued unused 'defer_recdef';

tuned;

removed dead code;

moved sources;

tuned proofs;

uniform system_mode for build test: avoid spurious output_dir/log that is not required later;

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

generalized some theorems about integral domains and moved to HOL theories

renamed multiset_of -> mset

NEWS

multiset_of_set -> mset_set

tuned proofs -- slightly faster;

merged

tuned proofs -- slightly faster;

tuned proofs -- much faster;

tuned proofs;

tuned

merged

added funs and lemmas

tuned proofs;

merged

manual merge;

tuned proofs;

isabelle update_cartouches;

avoid dynamic parsing of hardwired strings;

more compact name

NEWS

merged

renamed Multiset.set_of to the canonical set_mset

correccted the pretty-printing specs for setsum and setprod

New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.

another messy proof fixed

merged

more informative check: dummies are always allowed parse_term and should not lead to rejection here;

vacuous fact `TERM x`;

tuned signature;

inverted another messy proof

redundant: read = check o parse;

tuned;

moved sections;

moved sections;

tuned;

more robust: variables need not occur in body;

tuned;

tuned whitespace;

merged

improved treatment of Element.Obtains via Expression.prepare_stmt; discontinued pointless all_types ctxt: prep_var is always sequential;

clarified context; tuned;

tuned comment;

another tangled proof

Merge

Tidied up more proofs

merged

more examples;

tuned signature;

tuned;

another proof

fixing more proofs

Merge

Merge

fixed another horrible proof

tuned proofs;

tuned signature;

merged

more on 'consider' and related concepts;

tuned proofs;

tuned proofs;

open parameters for 'consider' rule;

implicit rule for method "cases";

eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

clarified 'obtain', using structured 'have' statement;

tuned comments;

clarified 'consider', using structured 'have' statement;

more examples;

renamed "prems" to "that";

support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;

made SML/NJ happy;

support to parse obtain clause without type-checking yet; tuned signature;

tuned -- eliminated unused feature;

tuned signature;

tuned;

streamlined many more proofs

Merge

tidied more proofs

proper subclass instances for existing gcd (semi)rings

slight preference for American English

generalized euclidean ring prerequisites

simplified relationship between associated and is_unit

proof tidying

CONTRIBUTORS

tuned lemmas and proofs

given up trivial definition

dropped warnings by dropping ineffective code declarations

standardized algebraic conventions: prefer a, b, c over x, y, z

uniform _ div _ as infix syntax for ring division

fixed several "inside-out" proofs

add transfer theorems for fixed points

Merge

tidied more proofs

misc tuning;

misc tuning;

unused;

misc tuning;

isabelle update_cartouches;

more user aliases;

merged

prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;

tuned proofs;

clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';

support for "if prems" in local goal statements;

tuned message;

tuned proofs;

no need for protected goal (see 240ad53041c9);

tuned proofs;

prevent export of future result -- avoid interference with goal fixes;

more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;

tuned signature;

allow for_fixes for 'have', 'show' etc.; tuned signature;

eliminated dead code;

clarified abstracted term bindings (again, see c8384ff11711);

tuned signature;

tuned;

clarified term bindings;

tuned

Merge

tuned

Renaming multiset operators < ~> <#,...

more tidying up of proofs

tidying messy proofs

tidying messy proofs

merged

clarified context;

tuned;

clarified abstracted term bindings;

avoid duplicate warning due to Variable.warn_extra_tfrees;

clarified Proof_Context.cert_propp/read_propp; tuned;

more careful treatment of term bindings in 'obtain' proof body; tuned signature;

tuned signature;

Merge

Tidied lots of messy proofs

tuned signature;

tuned (see also 66e6c539a36d);

tuned signature;

clarified: declare props once and for all; tuned signature;

tuned signature;

tuned signature;

tuned signature;

tuned;

tuned;

tuned;

tuned whitespace;

more tight treatment of subgoals: main goal may refer to extra variables;

added Isar command 'supply';

tuned;

clarified signature -- better support for Isar commands outside of Pure;

merged

clarified context;

tuned;

clarified context;

cleaified context; more uniform context data; tuned;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

tuned proof;

merged

simps_of_case: Better error if split rule is not an equality

simps_of_case: allow Drule.dummy_thm as ignored split rule

implicit partial divison operation in integral domains

separate class for division operator, with particular syntax added in more specific classes

explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer

dropped dead config option

tuned, including proper signature for functor argument

dropped dead code

explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations

explicit input marker for operations

completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept

self-contained formulation of abbrev for named targets

correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections

separate function to compute exported abbreviation

clearly separated target primitives (target_foo) from self-contained target operations (foo)

tuned order

dedicated config options to deactivate uncheck phase for improvable syntax

clarified interfaces for improvable syntax

tuned

clarified context;

clarified context;

clarified context;

tuned;

discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;

discontinued legacy;

obsolete (see 189c81779a68);

eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;

clarified context;

clarified context;

tuned;

clarified context;

tuned;

obsolete;

clarified context;

tuned;

tuned;

standardize towards Thm.eta_long_conversion, which just does eta_long conversion;

tuned spelling;

unused;

tuned;

more explicit context;

obsolete;

tuned -- more direct Thm.renamed_prop;

tuned message;

tuned whitespace;

removed model checks from Nitpick

document Nitpick issue

uncountability: open interval equivalences

Convex hulls: theorems about interior, etc. And a few simple lemmas.

made Auto Sledgehammer behave more like the real thing

took out Sledgehammer minimizer optimization that breaks things

modernized (slightly) type compiler in MicroJava

New material about paths, and some lemmas

removed obsolete RC tags;

merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;

Added tag Isabelle2015 for changeset 5ae2a2e74c93

clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;

updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;

tuned;

tuned;

updated versions;

tuned;

tuned;

cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;

more on displays with very high resolution;

add Haskabelle-2015 component

Added tag Isabelle2015-RC5 for changeset d7f636331176

added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;

updated Eisbach, using version 134bc592909c of its Bitbucket repository;

tuned;

updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;

clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";

tuned whitespace;

more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;

Added tag Isabelle2015-RC4 for changeset 05fe9bdc4f8f

new CVC4 component

took out unreliable 'blast' from tactic altogether

clarified tooltip;

sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;

more standard command setup;

silence local Unify.trace_bound as well: existing tools either refer to Proof.context or theory;

more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties); clarified Isabelle.buffer_token_marker;

use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;

no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;

updated screenshot;

tuned;

less confusing default;