added signature

moved thms_of_name to Sledgehammer_Util and removed copies, updated references

removed duplicate decleration

made use of sledgehammer_util

renamed sledgehammer_isar_reconstruct to sledgehammer_proof

added comments to new source files

fixed problem with fact names

remove hack and generalize code slightly

simplified isar_qualifiers and qs merging

put shrink in own structure

put annotate in own structure

support assumptions as facts for preplaying

some minor improvements in shrink_proof

some support for ML runtime statistics;

prefer tight Markup.print_int/parse_int for property values;

clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);

eliminated slightly odd identifiers;

tuned syntax, potentially more robust;

smarter list layout;

repaired text following 491c5c81c2e8;

merged

introduce filter_lim as a generatlization of tendsto

merged

based countable topological basis on Countable_Set

qualified interpretation of sigma_algebra, to avoid name clashes

eliminated finite_set_sequence with countable set

support for sub-structured identifier syntax (inactive);

eliminated some improper identifiers;

add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)

tuned signature; tuned;

more uniform Symbol.is_ascii_identifier in ML/Scala;

tuned;

clarified Symbol.scan_ascii_id; ATP: follow change from Symbol.scan_id to Symbol.scan_ascii_id, assuming that this was meant here, not fully symbolic Isabelle identifiers;

tuned;

convenience operations for table as set;

removed remains of Oheimb's double-space (cf. 0a5af667dc75);

tuned;

merged

updated two components

simplify code slightly

avoid non-ASCII sign

generate a parameterized correspondence relation

quot_thm_crel

add option_fold

add binomial_ge_n_over_k_pow_k

removed tool that was never finished

added file headers

updated MaSh doc

moved MaSh's Python code into Isabelle

updated NEWS etc.

distinguish declated tfrees from other tfrees -- only the later can be optimized away

clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;

reset active areas on content update;

more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';

tuned command descriptions;

refined outer syntax 'help' command;

tuned signature;

always reset active areas;

no special treatment of control_reset, in accordance to other control styles;

tuned signature;

tuned signature;

tuned signature;

tuned signature; uniform view.fontsize fallback;

renamed main plugin object to PIDE;

tuned signature -- avoid intrusion of module Path in generic PIDE concepts;

explicit module UTF8;

tuned file name;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

prefer strict error;

quasi-abstract module Rendering, with Isabelle-specific implementation;

added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;

eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;

retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;

prefer buffer_edit combinator over Java-style boilerplate;

more robust font for control symbols, to ensure these obscure codepoints are properly rendered;

tuned symbol groups;

tuned -- Symbol.groups already sorted;

more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;

added option jedit_symbols_search_limit;

avoid empty tooltip;

tuned symbol groups;

special handling of control symbols in Symbols dockable; less obscure Scala names;

recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;

avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);

more NEWS/CONTRIBUTORS;

improved editing support for control styles; separate module for Isabelle actions;

added ISABELLE_PLATFORM_FAMILY;

merged

moved lemma

timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);

add quotient_of_div

generate correct names

simplified code

generate correct correspondence relation name

more uniform title, follow-up to 928cb8b35e6e;

tuned

defer interpretation of markup via implicit print mode;

merged

made SML/NJ happier

pack window before accessing its geometry;

always refresh font metrics, to help window size calculation (amending 2585c81d840a);

more precise tooltip window size;

take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;

reset active area for outdated snapshot (again?);

some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;

more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;

some support for breakable text and paragraphs; tuned Symbol.scanner, which operates on symbols, not characters;

tuned names

tuned comment;

clarified symbol groups, despite this traditional arrangement in X-symbol grid;

always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;

tuned whitespace;

merged

included abbrev in tooltip

removed (unicode) tooltips: can not adjust font in basic swing tooltip

delayed search to improve reactivity

respect font property for symbols

capitalize lowercase groups; tuned with mkString

merged

more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML; more generous timeout for HOL-Quickcheck_Examples, which is rather slow in checking its examples (and mostly sequential);

Countable_Set: tuned lemma names; more generic lemmas

enable Symbols dockable by default;

tuned;

accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;

renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set

dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; search field for symbols

CONTRIBUTION: add fabians work

NEWS: document changes in HOL-Probability

NEWS (changeset 13211e07d931): add Countable_Set

NEWS (changeset 69b35a75caf3): document changes in FuncSet

new theory of immutable arrays

some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;

support for symbol groups, retaining original order of declarations; updated WWW_Find: untested change of ad-hoc parser of ~~/etc/symbols;

tuned;

add Countable_Set theory

tuned proof

simplified command line of "isabelle install";

known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);

some documentation for "algebra" in HOL;

global default for session timeout;

alternative completion for outer syntax keywords;

init options on startup as well;

theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;

tuned: use induction rule sigma_sets_induct_disjoint

tuned FinMap

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

more refs;

isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release); always generate sty files, as before c5d0f19ef7cb;

proper jvmpath for windows;

more generous tracing_limit, with explicit system option;

adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;

update options via protocol; jEdit dialog for "Parallel Checking" options;

more accurate pixel_range -- do not round offset here;

tuned signature;

prefer absolute default $USER_HOME/Scratch.thy;

more portable process exit;

tuned -- eliminate pointless ML method definition;

tuned;

NEWS;

tuned structure of Isabelle/HOL;

method setup for Classical steps;

tuned signature;

updated keywords;

moved (b)choice_iff(') to Hilbert_Choice

move theorems to be more generally useable

merged

made SML/NJ happy;

renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space

renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

measurability for nat_case and comb_seq

rules for AE and prob

rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication

more measurability rules

renamed to more appropriate lim_P for projective limit

allow arbitrary enumerations of basis in locale for generation of borel sets

repaired slip accidentally introduced in 57209cfbf16b

prefer implementation in HOL; n.b. code_reflect cannot reflect type synonyms

corrected headers

hide constants of auxiliary type finmap

generalized to copy of countable types instead of instantiation of nat for discrete topology

added projective limit; proof is based on auxiliary type finmap::polish_space

regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards

tuned -- eliminated obsolete citation of isabelle-ref;

updated basic equality rules;

removed somewhat pointless historic material;

updated unification options;

removed some historic material that is obsolete or rarely used;

tuned;

updated section on ordered rewriting;

updated subgoaler/solver/looper;

removed somewhat pointless historic material; tuned;

tuned;

updated explanation of rewrite rules;

(re)moved old material about Simplifier;

some coverage of "resolution without lifting", which should be normally avoided;

removed somewhat pointless historic material;

updated biresolve_tac, bimatch_tac; removed obscure historical material;

moved classical wrappers to IsarRef; removed somewhat pointless historic material;

avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");

updated citations;

tuned;

removed junk;

removed pointless historic material;

more on Simplifier rules, based on old material;

refurbished Simplifier examples;

more on the Simplifier, based on old material;

more concise/precise documentation;

tuned text

replaced relation by function - simplifies development

made SMLNJ happier

import Sublist rather than PrefixOrder to avoid unnecessary class instantiation

prefer explicit Random.seed

dropped dead code

tuned import order

tuned layout

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

create temp directory if not already created

merged

new theory IMP/Finite_Reachable

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

thread context correctly when printing backquoted facts

dropped dead code; tuned theory text

modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)

merged

fixed underscores

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

assume probability spaces; allow empty index set

added projective_family; generalized generator in product_prob_space to projective_family

moved lemmas further up

tuned proofs

using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier

hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call

NEWS

rewriting with the simpset that is passed to the simproc

handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc

tuned

syntactic tuning and restructuring of set_comprehension_pointfree simproc

using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls

improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones

adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc

handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc

simplified structure of patterns in set_comprehension_simproc

refined stack of library theories implementing int and/or nat by target language numerals

restored SML code check which got unintentionally broken: must explicitly check for error during compilation; restore more conventional namespace during check (relevant for Imperative-HOL)

add support for function application to measurability prover

renamed Sledgehammer option

always show timing for structured proofs

use implications rather than disjunctions to improve readability

avoid name clashes

fixed more "Trueprop" issues

removed needless sort

avoid double "Trueprop"s

use original formulas for hypotheses and conclusion to avoid mismatches

track formula roles in proofs and use that to determine whether the conjecture should be negated or not

correct parsing of E dependencies

proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction

tuned

code for while directly, not via while_option

executable true liveness analysis incl an approximating version

now that sets are executable again, no more special treatment of variable sets

handle non-unit clauses gracefully

several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)

use measurability prover

add measurability prover; add support for Borel sets

add syntax and a.e.-rules for (conditional) probability on predicates

infinite product measure is invariant under adding prefixes

for the product measure it is enough if only one measure is sigma-finite

Allow parentheses around left-hand sides of array associations

made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)

regenerated SMT certificates

regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles

fixed bool vs. prop mismatch

removed "refute" command from Isar manual, now that it has been moved outside "Main"

repaired "Mutabelle" after Refute move

less verbose -- the warning will reach the users anyway by other means

tuned messages

moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong

fixes related to Refute's move

added a timeout around script that relies on the network

took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly

moved Refute to "HOL/Library" to speed up building "Main" even more

tuning

use metaquantification when possible in Isar proofs

tuned code

tuning

soft SMT timeout

added function store_termination_rule to the signature, as it is used in Nominal2

longer log, to accomodate final status line of isabelle build;

transfer package: error message if preprocessing goal to object-logic formula fails

transfer package: add test to prevent trying to make cterms from open terms

transfer package: more flexible handling of equality relations using is_equality predicate

ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta

new theorems

incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy

close code theorems explicitly after preprocessing

tuned proofs;

further attempts to cope with large files via option jedit_text_overview_limit;

more detailed Prover IDE NEWS;

recovered explicit error message, which was lost in b8570ea1ce25;

removed dead code;

proper signatures;

tuned;

merged

Renamed {left,right}_distrib to distrib_{right,left}.

Tuned.

more conventional argument order; dropped dead code

another refinement in the comprehension conversion

refined simplifier call in comprehension_conv

passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls

avoid STIX font, which tends to render badly;

extra jar for scala-2.10.0-RC1;

more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;

avoid duplicate build of jars_fresh;

obsolete, cf. README_REPOSITORY;

accomodate scala-2.10.0-RC1;

tailored enum specification towards simple instantiation; tuned enum instantiations

refined internal structure of Enum.thy

moved quite generic material from theory Enum to more appropriate places

adding another test case for the set_comprehension_simproc to the theory in HOL/ex

improving tactic in setcomprehension_simproc

adjusting proofs

tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage

passing names and types of all bounds around in the simproc

locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree

more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;

merged

don't include Quotient_Option - workaround to a transfer bug

ignore old stuff and thus speed up the script greatly;

proper find -mtime (file data) instead of -ctime (meta data);

made SML/NJ happy;

clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);

back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;

merged

back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;

more basic Goal.reset_futures as snapshot of implicit state; more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

tuned proof;

update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer

tuned proofs

new theorem

merged

merged

merged

merged

fixed proof (cf. a81f95693c68);

tuned Isar output

tuned

updated docs

renamed Isar-proof related options + changed semantics of Isar shrinking

tuning

fixed theorem lookup code in Isar proof reconstruction

tuning

refactor code

tuning

more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);

collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;

tuned message;

tuned comment;

avoid spurious "bad" markup for show/test_proof; tuned;

more official Future.terminate; tuned signature;

simp results for simplification results of Inf/Sup expressions on bool; tuned proofs

no sort constraints on datatype constructors in internal bookkeeping

HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);

merged

comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic

checking for bound variables in the set expression; handling negation more generally

set_comprehension_pointfree simproc now handles the complicated test case; tuned

refined conversion to only react on proper set comprehensions; tuned

moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)

employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc

another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);

more robust cancel_now: avoid shooting yourself in the foot;

more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;

proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;

added Output "Detach" button;

skipped proofs appear as "bad" without counting as error;

more method position information, notably finished_pos after end of previous text;

more formal markup;

tuned signature; prefer exception Fail for internal errors;

more formal markup;

don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule

merged

added missing file

tuned for document output

added proof minimization code from Steffen Smolka

tuned blank lines

tuned whitespace

a few notations changed in HOL/BNF/Examples/Derivation_Trees

ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package

adding test cases for f x y : S patterns in set_comprehension_pointfree simproc

tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

extending preprocessing of simproc to rewrite subset inequality into membership of powerset

update ROOT with teh directory change in BNF

changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees

retain info dockable state via educated guess on window focus;

support for more informative errors in lazy enumerations;

more informative errors for 'also' and 'finally';

tuned messages;

more proof method text position information;

clarified defer/prefer: more specific errors;

updated Toplevel.proofs;

more informative errors for 'proof' and 'apply' steps; more Seq.result operations;

more friendly handling of Pure.thy bootstrap errors;

more informative error for stand-alone 'qed';

further attempts to unify/simplify goal output;

more informative error messages of initial/terminal proof methods; more systematic support for sequences with embedded errors; tuned Seq.maps;

merged

setcomprehension_pointfree simproc also works for set comprehension without an equation

tuned message -- avoid extra blank lines;

updated to polyml-5.5.0 which reduces chance of HOL-IMP failure (although it is hard to reproduce anyway);

store colors after build

adding further test cases for the set_comprehension_pointfree simproc

refined tactic in set_comprehension_pointfree simproc

adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully

adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc

extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned

more informative error of initial/terminal proof steps;

some attempts to unify/simplify pretty_goal;

refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;

tuned signature;

improved adhoc height for small fonts;

further refinement of jEdit line range, avoiding lack of final \n;

more uniform tooltip color;

more NEWS;

merged

disambiguated grammar

tuned proofs

tuned

simplified 'typedef' specifications: discontinued implicit set definition and alternative name;

discontinued typedef with alternative name;

discontinued obsolete typedef (open) syntax;

discontinued typedef with implicit set_def;

merged

increading indexes to avoid clashes in the set_comprehension_pointfree simproc

no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;

do not treat interrupt as error here, to avoid confusion in log etc.;

more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;

refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;

merged

cleanup borel_measurable_positive_integral_(fst|snd)

msetprod based directly on Multiset.fold; pretty syntax for msetprod_image

avoid global interpretation

simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets

clarified output token markup (see also bc22daeed49e);

refined aprop_tr' -- retain entity information by using type slot as adhoc marker;

refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x"; tuned;

tuned;

tuned;

more position information for hyperlink and placement of message;

tuned;

mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml

removed unused legacy material from mira.py

eliminated some remaining uses of typedef with implicit set definition;

merged

fix code equation for RBT_Impl.fold

merged

tail-recursive implementation for length

correct definition for skip_black

merged

merged

infprod generator works also with empty index set

add finite entropy

continuous version of mutual_information_eq_entropy_conditional_entropy

add induction for real Borel measurable functions

induction prove for positive_integral_fst

strong nonnegativ (instead of ae nn) for induction rule

induction prove for positive_integral_density

add induction rules for simple functions and for Borel measurable functions

introduce induction rules for simple functions and for Borel measurable functions

joint distribution of independent variables

indep_vars does not need sigma-sets

simplified definitions

remove unnecessary assumption from conditional_entropy_eq

alternative definition of conditional entropy

remove unneeded assumption from conditional_entropy_generic_eq

add induction rule for intersection-stable sigma-sets