generalized MaSh exporter to sets of theories

remove SMT proofs in Multivariate_Analysis

prove tendsto_power_div_exp_0 * * * missing rename

add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2

merged

emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);

go back to Z3 3.2

tuned defs of sec_xyz

provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;

simplify MaSh term patterns + add missing global facts if there aren't too many

MaSh improvements: deeper patterns + more respect for chained facts

tuned names

tweaked MaSh exporter

renamed "Type.thy" to something that's less likely to cause conflicts

proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)

added "fact_filter" option to Mirabelle

tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)

some notes on the Isabelle component repository at TUM;

use filterlim in Lim and SEQ; tuned proofs

conversion rules for at, at_left and at_right; applied to l'Hopital's rules.

weakened assumptions for lhopital_right_0

tuned proof

add L'Hôpital's rule

add filterlim rules for exp and ln to infinity

add filterlim rules for inverse and at_infinity

add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image

add filterlim rules for unary minus and inverse

rename filter_lim to filterlim to be consistent with filtermap

add check to Cooper's algorithm that left-hand of dvd is a numeral

merged

robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

avoid odd warnings due to failure of systray icon;

synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;

tuned;

recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32; tuned message;

semi-automated Cygwin setup;

misc tuning;

updated to sumatra_pdf-2.1.1;

tuned order of functions

proper quoting of paths in MaSh

updated to jedit_build-20121201 (based on jedit-5.0.0);

moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;

leave ALTERNATIVE_DISPATCHER mostly enabled on Mac OS X, to get events for COMMAND/Meta combinations, which seem to produce only KEY_PRESSED in Java 7, not KEY_TYPED as in Java 6;

updated to jedit-5.0.0;

more generic directory name to facilitate tracking changes of diffs;

merged

tuned

added 'print_inductives' command;

print formal entities with markup;

tuned labels;

renamed dockable "Prover Session" to "Theories"; more uniform Library.lowercase/uppercase;

tuned import;

alternative shortcut for English keyboard;

merged

eliminated redundant is_ident -- more official is_identifier;

updated to jdk-7u9;

updated to exec_process-1.0.3;

report proper pid *after* fork;

prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;

more defensive retry via fork;

merged

parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned

simplified use of fold/map; tuned;

tuned;

prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);

merged

make SML/NJ happy (give names for all fields in a record)

more robust syntax that survives collapse of \<^isub> and \<^sub>;

further update and clarification of the all-important README_REPOSITORY;

more uniform ML statistics;

merged

improved readability

tweaked calculation of sledgehammer messages

adapted sledgehammer warnings

fixed case split preplaying

fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup

preplay case splits

added warning when shrinking proof without preplaying

deal with the case that metis does not time out, but fails instead

reapplied changes to make SML/NJ happy

renaming, minor tweaks, added signature

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;