observe base URL of rendered document; added PIDE logo;

more README;

tuned README.html;

tuned;

retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);

tuned message, which is displayed after termination of Isabelle.app on Mac OS;

keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";

tuned;

ensure Isabelle env;

Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147

tuned;

misc tuning for release;

reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;

makedist for release;

put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes

require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0

put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod

adding an example with inductive predicates to quickcheck narrowing examples

importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck

clarify platforms

killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore

updated Nitpick SAT Solver doc

update list of SAT solvers reflecting Kodkod 1.5

tuned signature;

more uniform defaults;

Quotient_Set.thy is part of library

fixed typo

standardize drive letters -- important for proper document node identification;

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);