more robust handling of emacs options -- this is not necessarily an Isabelle process environment yet;

merged

actually invoke ISABELLE_TOOL;

added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;

ISABELLE_USEDIR_OPTIONS: less ambitious -M1 by default -- multithreading is largely untested on fringe platforms (cygwin, solaris);

misc updates for Isabelle2009;

Added tag isa2009-test for changeset dda08b76fa99

updated official title of contribution by Johannes Hoelzl;

misc tuning and updates;

updated doc setup;

merged

moved generated eps/pdf to main directory, for proper display in dvi;

updates for E-1.0-004;

tuned manual

merged

tuned comment

Added tag isa2009-test for changeset 613c2eb8aef6

tuned whitespace

merged

reverted to explicitly check the presence of a refutation (compare to 479a2fce65e6); simplified handling of errors in remote script

tuned white space;

merged

\nolinkurl for dvi mode recovers hyphenation of URLs -- this already works by default in PDF mode;

removed obsolete website directory -- information derived by website/build;

More precise treatement of rational constants by the normalizer for fields

fixed usage of rational constants

No Complex_Main needed

now deals with devision in fields

fixed formal markup;

merged

Finite_Set: lemma IsarRef: attribute arith

single-threaded build; misc tuning and simplification;

merged

Added check whether argument types of inductive set agree with types of declared parameters to avoid low-level error messages.

added setsum_eq_1_iff

simplified website/config;

Updated to corrected E output messages

updated keywords (with polyml-experimental);

some more HOL-Nominal news;

merged

tuned signature;

misc tuning for release;

merged

Fixed bug in transformation of congruence rule for == (thanks to Andy Schropp for reporting this).

some HOL-Nominal news;

updates for Isabelle2009 release;

tuned;

merged

misc cleanup and rearrangements for Isabelle2009 release;

merged

cleaned up setprod_zero-related lemmas

merged

generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs

added nat_div_gt_0 [simp]

added setsum_pos_nat

merged

added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas

proper external tikz pictures

merged

tuned comments;

merged

explicitly check that at least one argument is present to avoid low-level exception

merged

included managing_thread in state of AtpManager: synchronized termination and check for running managing_thread

domain package registers induction rules

merged

Merged.

Improvements to the text.

fixed header; misc simplification, use Conjunction.dest_conjunctions;

fixed header;

added dest_conjunctions (cf. Logic.dest_conjunctions);

superficial tuning;

merged

merged

schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;

updated latex requirement;

tuned document;

replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp); modernized and tuned document;

tuned error message;

tuned;

suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;

generalized pull to anamorph

merged

ML snippets for experimental evaluation

merged

merged

domain package declares more simp rules

simplified 'print_orders' command;

tuned;

merged

merged

simplify theorem references

added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);

tuned spacing and formatting;

merged

terminate watching thread

merged

no longer delay loading of assoc_fold.ML

qualified_name_of: observe empty case;

merged

merged

add more lemmas for signed comparisons

use standard parsers provided by SpecParse

bstring -> binding

code attribute for tailrec-equations, too; tuned

optimistically add code attribute to .simps without further checks

remove "otherwise" feature from function package which was never really documented or used

prep_full_context_statement: explicit record of flags; prep_declaration (for add_locale): disallow autofixed frees;

Limit the number of results returned by auto_solves.

merged

Merged.

In interpretation: equations are not propagated through the hierarchy automatically.

Normalise equation only for morphism, not thm stored in theory.

Default mode of qualifiers in locale commands.

Front matter updated.

tuned;

simplified Element.activate(_i): singleton version;

tuned;

added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;

unified binding prefix terminology;