more user aliases;

fixed IsaMakefile action for HOL-TPTP.

prefer socket comminication on Cygwin, which is more stable here than fifos;

tuned proof;

made SML/NJ happy;

discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);

updated header;

merged;

reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)

first step towards extending Minipick with more translations

Include keywords print_coercions and print_coercion_maps

local coercion insertion algorithm to support complex coercions

printing and deleting of coercions

raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;

default print mode for Isabelle/Scala, not just Isabelle/jEdit;

augment existing print mode;

explicit option for socket vs. fifo communication;

tuned proof;

synchronized section names with manual

merged;

discontinued legacy theorem names from RealDef.thy

merged

discontinued HOLCF legacy theorem names

take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime

Moved extraction part of Higman's lemma to separate theory to allow reuse in theories compiled without support for proof terms.

Removed hcentering and vcentering options, since they are not supported by all versions of geometry.

merged

Added documentation for HOL-SPARK

drop partial monomorphic instances in Metis, like in Sledgehammer

better type reconstruction -- prevents ill-instantiations in proof replay

NEWS: mention replacement lemmas for the removed ones in Complete_Lattices

changing quickcheck_timeout to 30 seconds in mutabelle's testing

adding post-processing of terms to narrowing-based Quickcheck

HOL/ex/ROOT.ML: only list BinEx once

merged

remove redundant instantiation ereal :: power

reintroduced Minipick as Nitpick example

tuned comment

merged

Extended_Real_Limits: generalize some lemmas

add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;

made SML/NJ happy;

abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;

alternative Socket_Channel; use BinIO for fifos uniformly;

more abstract wrapping of fifos as System_Channel;

slightly more general Socket_IO as part of Pure;

more hints on Z3 configuration;

reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);

renamed inv -> filter

Added proofs about narowing

added missing makefile dependence

added example

tuned

refined comment

fixed two typos in IMP (by Jean Pichon)

merged

Updated IMP to use new induction method

New proof method "induction" that gives induction hypotheses the name IH.

official status for UN_singleton

tuned specification and lemma distribution among theories; tuned proofs

more careful treatment of initial update, similar to output panel;

proper fact binding;

syntactic improvements and tuning names in the code generator due to Florian's code review

match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test

fixed headers;

less ambiguous syntax;

tuned proofs;

merged

catch PatternMatchFail exceptions in narrowing-based quickcheck

removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition

ensuring that some constants are generated in the source code by adding calls in ensure_testable

adding abstraction layer; more precise function names

adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used

determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations

only annotating constants with sort constraints

also adding type annotations for the dynamic invocation

removed legacy lemmas in Complete_Lattices

increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling

more isatest stats;

refined Symbol.is_symbolic -- cover recoded versions as well;

double clicks switch to document node buffer;

tuned;

explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);

at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;

instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);

unique file names via serial numbers, to allow files like "root" or multiple files with same base name;

imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;

merged

numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else

removed obsolete patches for PG 4.1;

additional space for borderless UI;

more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);

explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;

isatest settings for macbroy6 (Mac OS X Lion);

more Mac OS reference hardware;

updated to SML/NJ 110.73;

tentative announcement based on current NEWS;

tuned;

separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

updated for release;

tuned;

updated generated file;

updated Complete_Lattices;

some tuning and re-ordering for release;

misc tuning for release;

more contributors;

tuned proofs;

tweak keyboard shortcuts for Mac OS X;

explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;

finite sequences as useful as introductory example;

discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;

graph traversal in topological order; Session.snapshot() with sensible defaults;

Document.Node.Name convenience;

more precise painting;

more elaborate Node_Renderer, which paints node_name.theory only;

raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;

tuned signature;

more careful traversal of theory dependencies to retain standard import order;

sane default for class Thy_Load;

removed obsolete patches for PG 4.1;

specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;

added "isabelle scalac" convenience;

Symbol.explode as in ML;

ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;

dropped unused argument – avoids problem with SML/NJ

tuned spacing

tuned

tuned post fixpoint setup

merged

when applying induction rules, remove names of assumptions that come with the rule in case the rule is transformed by the simplifier due to instantiations

remove stray "using [[simp_trace]]"

tune indenting

removed unused legacy lemma names, some comment cleanup.

removed word_neq_0_conv from simpset, it's almost never wanted.

removed further legacy rules from Complete_Lattices

NEWS on Complete_Lattices, Lattices

tail recursive proof preprocessing (needed for huge proofs)

tuning

merged

revised AbsInt and added widening and narrowing

updated comment

updated generated code

tuned

renamed Complete_Lattices lemmas, removed legacy names

merged

create central list for language extensions used by the haskell code generator

observe distinction between sets and predicates

merged

cleand up AbsInt fixpoint iteration; tuned syntax

tuned proofs

tuned proofs

remove some redundant [simp] declarations; simplify some proofs;

tune proofs

tune simpset for Complete_Lattices

merged

added lemma motivated by a more specific lemma in the AFP-KBPs theories

simplified unsound proof detection by removing impossible case

correcting NEWS

correcting theory name and dependencies

renamed AList_Impl to AList

fastsimp -> fastforce in doc

fix typo

shorten proof of frontier_straddle

NEWS and CONTRIBUTORS

remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def

simplify proofs using LIMSEQ lemmas

remove trivial lemma Lim_at_iff_LIM

fix typos

NEWS for euclidean_space class

move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

adding NEWS and CONTRIBUTORS

merged

correcting imports after splitting and renaming AssocList

tuned

moving connection of association lists to Mappings into a separate theory

adding NEWS and CONTRIBUTORS

tuned some symbol that probably went there by some strange encoding issue

added my contributions to NEWS and CONTRIBUTORS

fixed type intersection (again)

consistent option naming

NEWS fastsimp -> fastforce

new fastforce replacing fastsimp - less confusing name

merged

NEWS for Library/Product_Lattice.thy

misc tuning and clarification;

merged

merged

tuned proofs

Library/Saturated.thy: 'Sat' abbreviates 'of_nat'

more CONTRIBUTORS;

persistent ISABELLE_INTERFACE_CHOICE;

explicit choice of interface;

more orthogonal signature;

updates for release;

misc tuning and clarification (NB: settings are already local for named snapshots/releases);

some updates of PLATFORMS;

more README;

merged

mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)

misc tuning;

misc tuning and clarification;

speed up slow proof;

merged

more modularization

stronger colors (as background);

some color scheme for theory status;

some keyboard shortcuts for important actions; proper label properties, which are also required for jEdit "Shortcuts" options panel;

explicit jEdit actions -- to enable key mappings, for example;

more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;

tuned usage;

simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);

renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.

fixed definition of type intersection (soundness bug)

continue with minimization in debug mode in spite of unsoundness

generalize lemma of_nat_number_of_eq to class number_semiring

merged

stating more explicitly our expectation that these two terms have the same term structure

revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types

made SML/NJ happy

call ghc with -XEmptyDataDecls

merged

tuned headers

Library/Saturated.thy: number_semiring class instance

remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}

merged

remove unnecessary intermediate lemmas

added syntactic classes for "inf" and "sup"

prove existence, uniqueness, and other properties of complex arg function

tuned

remove obsolete intermediate lemma complex_inverse_complex_split

tuned

merged

tuned

merged

merged

merged

merged

merged

tuned

merged

tuned

tuned

fixed computation of "in_conj" for polymorphic encodings

add some new lemmas about cis and rcis; simplify some proofs;

Complex.thy: move theorems into appropriate subsections

merged

remove redundant lemma complex_of_real_minus_one

simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma

removed unused lemma sin_cos_squared_add2_mult

remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq

avoid using legacy theorem names

merged

theory of saturated naturals contributed by Peter Gammie

theory of saturated naturals contributed by Peter Gammie

lemmas about +, *, min, max on nat

update Sledgehammer docs

added new tagged encodings to Metis tests

also implemented ghost version of the tagged encodings

added new guards encoding to test

smarter explicit apply business

started work on ghost type arg encoding

stricted type encoding parsing

more substructural sharing to gain significant compression;

XML.cache for partial sharing (strings only);

platform-specific look and feel;

more README;

clarified terminology;

no print_state for final proof commands, which return to theory state;

NEWS on IsabelleText font;

explicit join_syntax ensures command transaction integrity of 'theory';

some updates for release;

some tuning for release;

updated file locations;

merged

merged

removing previously used function locally_monomorphic in the code generator

setting const_sorts to false in the type inference of the code generator

adapting Imperative HOL serializer to changes of the iterm datatype in the code generator

removing previous crude approximation to add type annotations to disambiguate types

adding minimalistic implementation for printing the type annotations

adding call to disambiguation annotations

adding type inference for disambiguation annotations in code equation

adding the body type as well to the code generation for constants as it is required for type annotations of constants

changing const type to pass along if typing annotations are necessary for disambigous terms

fixed THF type constructor syntax

tweaking polymorphic TFF and THF output

parse new experimental '@' encodings

tuning

tuning

tuning

clarified import;

tuned/simplified proofs;

tuned proofs;

deactivate unfinished charset provider for now, to avoid user confusion;

more NEWS;

added "check" button: adhoc change to full buffer perspective;

added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);

separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed

perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s

tuning

make mangling sound w.r.t. type arguments

make "filter_type_args" more robust if the actual arity is higher than the declared one

updated Sledgehammer documentation

rationalize uniform encodings

merged

avoid using legacy theorem names

merged

remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared

HOL/Import: Update HOL4 generated files to current Isabelle.

tuned proofs;

remove some unnecessary simp rules from simpset

some Isabelle/jEdit NEWS;

more README;

merged

merged

simplify proof of tan_half, removing unused assumptions

convert some proofs to Isar-style

added dummy polymorphic THF system

added some examples for pattern and weight annotations

merged

avoid "Code" as structure name (cf. 3bc39cfe27fe)

remove duplicate copy of lemma sqrt_add_le_add_sqrt

remove redundant lemma real_sum_squared_expand in favor of power2_sum

remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

merged

add lemmas about arctan; simplify some proofs about arctan;

convert lemma cos_total to Isar-style proof

added new lemmas

updated Sledgehammer's docs

cleanup "simple" type encodings

merge

HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.

tuning

drop more type arguments soundly, when they can be deduced from the arg types

bulk reports for improved message throughput;

bulk reports for improved message throughput;

tuned signature;

more specific message channels to avoid potential bottle-neck of raw_messages;

buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;

more abstract receiver interface;

flush after Output.raw_message (and init message) for reduced latency of important protocol events;

convert lemma cos_is_zero to Isar-style

merged

convert lemma sin_gt_zero to Isar style; remove duplicate lemma sin_gt_zero1;

modify lemma sums_group, and shorten proofs that use it

generalize some lemmas

add lemmas cos_arctan and sin_arctan

tuned indentation

more visible outdated_color;

commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;

tuned imports;

fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"

tuned

tuned

filter out all schematic theorems if the problem contains no ground constants

merged

tuned comments

simplify proof of Bseq_mono_convergent

merged

replace lemma expi_imaginary with reoriented lemma cis_conv_exp

remove redundant lemmas expi_add and expi_zero

remove redundant lemmas about LIMSEQ

introduce abbreviation 'int' earlier in Int.thy

remove unused assumptions from natceiling lemmas

move lemmas nat_le_iff and nat_mono into Int.thy

eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);

simplified signatures;

synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;

tuned document;

improved handling of extended styles and hard tabs when prover is inactive;

mark hard tabs as single chunks, as required by jEdit;

updated READMEs;

property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;

moved XML/YXML to src/Pure/PIDE; tuned comments;

pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);

pseudo-definition for perms on sets; tuned

remove duplicate lemma nat_zero in favor of nat_0

merged

merged

modify nominal packages to better respect set/pred distinction

merged

remove unused assumption from lemma posreal_complete

tuned specifications

merged