added type abstractions (for declaring polymorphic constants) to TFF syntax

implement more of the polymorphic simply typed format TFF(1)

flip logic of boolean option so it's off by default

extended simple types with polymorphism -- the implementation still needs some work though

added dummy PFF prover, for debugging purposes

first step towards polymorphic TFF + changed defaults for Vampire

tuning

removed explicit reliance on Hilbert_Choice.Eps

improved handling of induction rules in Sledgehammer

added generation of induction rules

simplify some proofs

restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);

tuned signature;

dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);

some support for hyperlinks between different buffers; tuned signature;

tuned colors -- more distance between outdated_color and quoted_color;

do not normalized extra file dependencies for now -- still loaded by prover process;

separate module for jEdit primitives for loading theory files;

merged

Product_Vector.thy: clean up some proofs

actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;

some dialog for auto loading of required files (still inactive);

invoke in Swing thread to make double sure;

move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;

generalize LIM_zero lemmas to arbitrary filters

merged

discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

tuned

split timeout among ATPs in and add Metis to the mix as backup

more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;

tuned positions of ambiguity messages -- less intrusive in IDE view;

tuned

merged

avoid loading List_Cset and Dlist_Cet at the same time

corrected slip

Cset, Dlist_Cset, List_Cset: restructured

Cset, Dlist_Cset, List_Cset: restructured

adapted to changes in Cset.thy

adapted to changes in Cset.thy

separating predicates and sets syntactically

merged

avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)

updated generated files

merged

updated generated files

explicit markup for legacy warnings;

updated generated files;

less aggressive warning icon;

tuned colors;

transparent foreground color for quoted entities;

more precise treatment of nodes that are fully required for partially visible ones;

de-assigned commands also count as changed;

beef up sledgehammer_tac in Mirabelle some more

merged

change default for generation of tag idempotence and tag argument equations

merged

NEWS entry for setsum_norm ~> norm_setsum

make HOL-Probability respect set/pred distinction

merged

use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)

merged

generalize and simplify proof of continuous_within_sequentially

add lemma sequentially_imp_eventually_within; rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;

replace some continuous_on lemmas with more general versions

remove legacy theorem Lim_inner

arrange everything related to ordered_euclidean_space class together

generalize and shorten proof of basis_orthogonal

remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}

merged

generalize lemma finite_imp_compact_convex_hull and related lemmas

generalize some lemmas

generalize lemma convex_cone_hull

rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;

simplify many proofs about subspace and span; reorder premises in rule span_induct;

remove duplicate simp declaration

simplify definition of 'interior'; add lemmas interiorI and interiorE; change lemmas interior_unique and closure_unique to rule_format; tidy some proofs;

add lemma closure_union; simplify some proofs;

minimize imports

move everything related to 'norm' method into new theory file Norm_Arith.thy

remove unused lemmas dimensionI, dimension_eq

move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used

merge

FSet: Explicit proof without mem_def

merged

added lemma

added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files

comment

disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP

improve completeness of polymorphic encodings

mangle tag bound declarations properly

fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings

make sure that if slicing is disabled, a non-SOS slice is chosen

honor TFF Implicit

make polymorphic encodings more complete

make default unsound mode less unsound

make TFF output less explicit where possible

use more appropriate encoding for Z3 TPTP, as confirmed by evaluation

added one more known Z3 failure

added config options to control two aspects of the translation, for evaluation purposes

added choice operator output for Satallax

rationalized option names -- mono becomes raw_mono and mangled becomes mono

handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards

avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics

fixed bang encoding detection of which types to encode

lemma Compl_insert: "- insert x A = (-A) - {x}"

avoid variable clashes by properly incrementing indices

improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

include chained facts for minimizer, otherwise it won't work

remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway

back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;

tuned Session.edit_node: update_perspective based on last_exec_offset;

tuned signature -- iterate subsumes both fold and get_first;

further clarification of Document.updated, based on last_common and after_entry; tuned;

tuned signature;

improved Document.edit: more accurate update_start and no_execs; tuned;

refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;

tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

maintain last_execs assignment on Scala side; prefer tables over IDs instead of objects;

propagate information about last command with exec state assignment through document model;

tuned signature;

slightly more abstract Command.Perspective;

slightly more abstract Text.Perspective;

tuned proofs;

tuned syntax -- avoid ambiguities;

more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");

delete commented-out dead code

merged

change some subsection headings to subsubsection

remove unnecessary lemma card_ge1

move connected_real_lemma to the one place it is used

merged

make sure that all facts are passed to ATP from minimizer

more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"

specify timeout for "sledgehammer_tac"

tuning

Quotient Package: add mem_rsp, mem_prs, tune proofs.

merged

declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;

merged

merged

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;