avoid warnings

comment out dead code to avoid compiler warnings

legacy theorem names

remove duplicate lemma

fixed "hBOOL" of existential variables, and generate more helpers

don't select facts when using sledgehammer_tac for reconstruction

don't perform a triviality check if the goal is skipped anyway

optional reconstructor

misc tuning and simplification;

tuned pri: prefer purging of canceled execution;

tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;

clarified Document.Node.clear -- retain header (cf. ML version);

clarified norm_header/header_edit -- disallow update of loaded theories;

misc tuning and simplification;

ignore irrelevant timings;

print state only for visible command, to avoid wasting resources for the larger part of the text;

early filtering of unchanged perspective;

more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);

update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;

tuned;

handle potentially more approriate BufferUpdate.LOADED event;

special treatment of structure index 1 in Pure, including legacy warning;

compile

added "max_calls" option to get a fixed number of Sledgehammer calls per theory

beef up "sledgehammer_tac" reconstructor

clean up Sledgehammer tactic

fixed document;

tuned signature;

merged

always use TFF if possible

clearer separator in generated file names

exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"

updated known failures for Z3 3.0 TPTP

updated Z3 docs

avoid TFF format with older Vampire versions

update the Vampire related parts of the documentation

fixed TFF slicing

kindly ask Vampire to output axiom names

added formats to the slice and use TFF for remote Vampire

tuned specifications, syntax and proofs

tuned specifications and syntax

Quotient Package: some infrastructure for lifting inside sets

include all encodings in tests, now that the incompleteness of some encodings has been addressed

change Metis's default settings if type information axioms are generated

we must tag any type whose ground types intersect a nonmonotonic type

prefer the lighter, slightly unsound monotonicity-based encodings for Metis

made reconstruction of type tag equalities "\?x = \?x" reliable

tuning ATP problem output

revert guard logic -- make sure that typing information is generated for existentials

generate tag equations for existential variables

tuning, plus started implementing tag equation generation for existential variables

precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis

clearer terminology

renamed "heavy" to "uniform", based on discussion with Nick Smallbone

removed unused configuration option

added caching for (in)finiteness checks

remove needless typing information

cleaner handling of polymorphic monotonicity inference

started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone

more precise warning

added option to control soundness of encodings more precisely, for evaluation purposes

make sound mode more sound (and clean up code)

reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

gracefully handle empty SPASS problems

pass sound option to Sledgehammer tactic

tuned signature -- contrast physical output primitives versus Output.raw_message;

tuned signature;

discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

some support for toplevel printing wrt. editor perspective (still inactive);

propagate editor perspective through document model;

some support for editor perspective;

discontinued redundant Edit_Command_ID;

reduced warnings;

tuned message;

old-style numbered structure index is legacy feature (hardly ever used now);

added official Text.Range.Ordering; some support for text perspective;

tuned signature;

reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

merged

modernized specifications

removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy

removed technical or trivial unused facts

more precise authors and comments; tuned order and headers

added proof of idempotence, roughly after HOL/Subst/Unify.thy

tuned proofs, sledgehammering overly verbose parts

tuned notation

ported some lemmas from HOL/Subst/*; tuned order

changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.

merged

add lemmas interior_Times and closure_Times

avoid pred/set mixture

avoid pred/set mixture

merged

remove unnecessary euclidean_space class constraints

section -> subsection

scale dependency graph to fit on page

more robust initialization of token marker and line context wrt. session startup;

tuned Parse.group: delayed failure message;

avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;

default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;

tuned;

discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;

discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;

merged

replace lemma realpow_two_diff with new lemma square_diff_square_factored

remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff

move lemma add_eq_0_iff to Groups.thy

remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead

rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy

add lemma power2_eq_iff

remove some over-specific rules from the simpset

merged

redefine constant 'trivial_limit' as an abbreviation

purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;

refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;

odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

clarified get_imports -- should not rely on accidental order within graph;

tuned Table.delete_safe: avoid potentially expensive attempt of delete;

discontinued "Interrupt", which could disturb administrative tasks of the document model;

more direct balanced version Ord_List.unions;

reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;

tuned future priorities (again);

clarified fulfill_norm_proof: no join_thms yet; clarified priority of fulfill_proof_future, which is followed by explicit join_thms; explicit Thm.future_body_of without join yet; tuned Thm.future_result: join_promises without fulfill_norm_proof;

added Future.joins convenience; clarified Future.map: based on Future.cond_forks;

merged

deactivated »unknown« nitpick example

merged

tuned proof

more uniform formatting of specifications

compatibility layer

merged

more concise definition for Inf, Sup on bool

do not call ghc with -fglasgow-exts

remove some redundant simp rules about sqrt

move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs

remove unused lemma DERIV_sin_add

remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong

remove redundant lemma exp_ln_eq in favor of ln_unique

merged

Lim.thy: legacy theorems

SEQ.thy: legacy theorem names

delete unused lemmas about limits

Transcendental.thy: add tendsto_intros lemmas; new isCont theorems; simplify some proofs.

add lemma isCont_tendsto_compose

merged

Transcendental.thy: remove several unused lemmas and simplify some proofs

remove unused lemmas

fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas

remove some redundant simp rules

maintain recent future proofs at transaction boundaries;

incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;

tuned;

tuned signature (again); tuned;

tuned signature -- treat structure Task_Queue as private to implementation;

refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;

Future.promise: explicit abort operation (like uninterruptible future job); explicit cancel_scala message -- still unused;

editable raw text areas: allow user to clear content;

more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;

more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;

clarified Future.cond_forks: more uniform handling of exceptional situations;

Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.

merged

define complex exponential 'expi' as abbreviation for 'exp'

remove more bounded_linear locale interpretations (cf. f0de18b62d63)

optimize some proofs

add Multivariate_Analysis dependencies

import Library/Sum_of_Squares instead of reloading positivstellensatz.ML

declare euclidean_component_zero[simp] at the point it is proved

Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.

merged;

merged

remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

merged

merged

avoid duplicated simp add option

observe distinction between sets and predicates more properly

moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace

avoid case-sensitive name for example theory

merged

case_names NEWS

adding documentation about simps equation in the inductive package

activating narrowing-based quickcheck by default

more precise treatment of exception nesting and serial numbers;

more careful treatment of exception serial numbers, with propagation to message channel;

updated sequential version (cf. b94951f06e48);

tuned comments;

tuned document; tuned proofs;

clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;

export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;

tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;

Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.

merged

HOL-IMP: respect set/pred distinction

Determinants.thy: avoid using mem_def/Collect_def

Wfrec.thy: respect set/pred distinction

follow updates of Isabelle/Pure;

merged

IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library

merged

Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems

add lemma tendsto_compose_eventually; use it to shorten some proofs

Topology_Euclidean_Space.thy: simplify some proofs

add lemma metric_tendsto_imp_tendsto

simplify proofs of lemmas open_interval, closed_interval

identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;

clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;

more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

tuned signature;

merged

merged

merged

avoid Collect_def in proof

modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;

improved default context for ML toplevel pretty-printing;

less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);

some convenience actions/shortcuts for control symbols;

export Function_Fun.fun_config for user convenience;

moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

distinguish THF syntax with and without choice (Satallax vs. LEO-II)

merged

add simp rules for isCont

updated keywords -- old codegen is no longer in Pure;

include HOL-Library keywords for the sake of recdef;

merged

Multivariate_Analysis includes Determinants.thy, but doesn't import it by default

get Multivariate_Analysis/Determinants.thy compiled and working again

get Library/Permutations.thy compiled and working again

workaround for Cygwin, to make it work in the important special case without extra files;

more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;

tuned message;

more robust treatment of node dependencies in incremental edits;

use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;

omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;

merged

generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space

add lemma tendsto_compose

remove extraneous subsection heading

generalized lemma closed_Collect_eq

remove duplicate lemma disjoint_iff

Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space

add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;

generalize lemma continuous_uniform_limit to class metric_space

remove duplicate lemmas eventually_conjI, eventually_and, eventually_false

Topology_Euclidean_Space.thy: organize section headings

simplify some proofs

generalize lemma convergent_subseq_convergent

locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses

locale-ize some constant definitions, so complete_space can inherit from metric_space

generalize constant 'lim' and limit uniqueness theorems to class t2_space

Quotient Package: make quotient_type work with separate set type

updated README;

touch descendants of edited nodes; more precise handling of Graph exceptions;

parellel scheduling of node edits and execution;

tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

HOL-Nominal-Examples: respect distinction between sets and functions

less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;

merged

HOL-Hahn_Banach: use Set_Algebras library

ex/Quickcheck_Examples.thy: respect distinction between sets and functions

clarified Toplevel.end_theory;

simplified Toplevel.init_theory: discontinued special name argument;

simplified Toplevel.init_theory: discontinued special master argument;

provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;

reduced verbosity;

tuned signature;

clarified node header -- exclude master_dir;

tuned;

maintain node header; misc tuning and clarification;

removed unused lemma; removed old-style ;

point isatest-statistics to the right afp log files

IMP/Util distinguishes between sets and functions again; imported only where used.

remove redundant lemma setsum_norm in favor of norm_setsum; remove finiteness assumption from setsum_norm_le;

merged

make more HOL theories work with separate set type

immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029); more careful treatment of last_round on startup/shutdown;

merged

merged

make Multivariate_Analysis work with separate set type

make HOLCF work with separate set type

merged

avoid duplicate rule warnings

modify euclidean_space class to include basis set

remove lemma stupid_ext

documented extended version of case_names attribute

normalized theory dependencies wrt. file_store;

general Graph.schedule;

allow "$" within basic path elements (NB: initial "$" refers to path variable);

clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

simplified class Thy_Header;

clarified Exn.message;

uniform treatment of header edits as document edits;

explicit datatypes for document node edits;

tuned;

disentangled nested ML files;

minimal script to run raw Poly/ML with concurrency library;

somewhat more uniform THIS;

more trimming;

recovered some ML toplevel pp;

some trimming;

prefix of Pure/ROOT.ML required for concurrency within the ML runtime;

redundant use of misc_legacy.ML;

eliminated use of recdef

removed obsolete recdef-related examples

removed unused material, which does not really belong here

merged

avoid warnings about duplicate rules

follow standard naming scheme for sgn_vec_def

remove several redundant and unused theorems about derivatives

remove redundant lemma

simplify proof of lemma bounded_component

simplify some proofs

more uniform naming scheme for finite cartesian product type and related theorems

move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy

merged

split Linear_Algebra.thy from Euclidean_Space.thy

full import paths

declare tendsto_const [intro] (accidentally removed in 230a8665c919)

merged

simplified definition of class euclidean_space; removed classes real_basis and real_basis_with_inner

bounded_linear interpretation for euclidean_component

lemma bounded_linear_intro

avoid duplicate rewrite warnings

mark some redundant theorems as legacy

Derivative.thy: more sensible subsection headings

Derivative.thy: clean up formatting

instance real_basis_with_inner < perfect_space

old term operations are legacy;

moved old code generator to src/Tools/;

avoid OldTerm operations -- with subtle changes of semantics;

avoid OldTerm operations -- with subtle changes of semantics;

avoid OldTerm operations -- with subtle changes of semantics;

avoid OldTerm operations -- with subtle changes of semantics;

tuned signature;

Goal.forked: clarified handling of interrupts;

future_job: explicit indication of interrupts;

more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;

synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;

tuned source structure;

bash_output_fifo blocks on Cygwin 1.7.x;

rename_bvs now avoids introducing name clashes between schematic variables

merged

tuned proofs

merged

tuned header

more uniform naming scheme for Inf/INF and Sup/SUP lemmas

removed "extremely ambigous" warning; has been ignored by everyone for years.

misc tuning and clarification;

tuned whitespace;

support local HOATPs

document local HOATPs

workaround THF parser limitation

LEO-II also supports FOF

misc tuning and simplification;

updated documentation of method "split" according to e6a4bb832b46;

updated references to CADE-23

renamed E wrappers for consistency with CASC conventions

updated Sledgehammer docs

add line number prefix to output file name

added "sound" option to Mirabelle

move lambda-lifting code to ATP encoding, so it can be used by Metis

load lambda-lifting structure earlier, so it can be used in Metis

merged

move legacy candiates to bottom; marked candidates for default simp rules

merged

dropped lemmas (Inf|Sup)_(singleton|binary)

dropped lemmas (Inf|Sup)_(singleton|binary)

rename type 'a net to 'a filter, following standard mathematical terminology

HOLCF: fix warnings about unreferenced identifiers

remove duplicate lemmas

merged

fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)

generalize sequence lemmas

generalize more lemmas about compactness

generalize compactness equivalence lemmas

lemma bolzano_weierstrass_imp_compact

class perfect_space inherits from topological_space; generalized several lemmas

merged

import constant folding theory into IMP

make syntax ambiguity warnings a config option

add lemmas INF_image, SUP_image

declare {INF,SUP}_empty [simp]

rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)

standard theorem naming scheme: complex_eqI, complex_eq_iff

moved division ring stuff from Rings.thy to Fields.thy

Library/Product_ord: wellorder instance for products

modernized file proof_checker.ML;

tuned thm_of_proof: build lookup table within closure;

added Reconstruct.proof_of convenience;

ship message in one piece;

misc tuning -- eliminated old-fashioned rep_thm;

modernized strcture Proof_Checker;

less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;

updated imports;

proper signature;

made SML/NJ happy;

slightly more uniform messages;

avoid pointless completion of illegal control commands;

removed old expand_fun_eq

fixed index entry

removed old recdef and types usage

merged

extended user-level attribute case_names with names for case hypotheses

infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names

workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;

updated version information;

fixed document;

tuned order: pushing INF and SUP to Inf and Sup

tuned order: pushing INF and SUP to Inf and Sup

generalized lemmas to complete lattices

merged

replace old SML code generator by new code generator in MicroJava/J

new state syntax with less conflicts

replace old SML code generator by new code generator in MicroJava/JVM and /BV

merged

more fine-granular instantiation

solving duality problem for complete_distrib_lattice; tuned

merged

Pending FDL types may now be associated with Isabelle types as well.

tuned orthography

avoid yet unknown fact antiquotation

NEWS

more specific instantiation

tuned

class complete_distrib_lattice

NEWS

removing value invocations with the SML code generator

removing the SML evaluator

fixed wrong isubs in IMP/Types

Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names

NEWS: fix typo

updated unchecked forward reference

replaced Nitpick's hardwired basic_ersatz_table by context data

NEWS

moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef

moved recdef package to HOL/Library/Old_Recdef.thy

added dynamic ersatz_table to Nitpick's data slot

eliminated obsolete recdef/wfrec related declarations

more consistent naming in IMP/Comp_Rev

merged

tuned proofs

tuned proofs

new theory HOL/Library/Product_Lattice.thy

domain package: more informative error message for illegal indirect recursion

compiler proof cleanup

added helpers for "All" and "Ex"

put parentheses around non-trivial metis call

no needless mangling

resolved code_pred FIXME in IMP; clearer notation for exec_n

clean up temporary directory hack

tuning

fixed lambda concealing

make SML/NJ happy

simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)

document coercions

rudimentary documentation of the quotient package in the isar reference manual

to_nat is injective on arbitrary domains

finite vimage on arbitrary domains

updated Sledgehammer documentation

renamed "preds" encodings to "guards"

more precise dependencies

further worked around LEO-II parser limitation, with eta-expansion

use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)

no need for existential witnesses for sorts in TFF and THF formats

mangle "undefined"

tuning -- remove useless function (at this point combinators are already in)

remove spurious message

give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts

merged

fixed code generator setup in List_Cset

enat is a complete_linorder instance

merged

Add theory for setting up monad syntax for Cset

merged