do not open ML structures;

updated scala; removed jedit -- component needs to be build afresh from ISABELLE_HOME/src/Tools/jEdit;

do not open ML structures;

do not open Codegen;

tuned whitespace, indentation, comments;

updated for release;

tuned;

more precise parentheses and indentation; eliminated trailing whitespace;

comments;

updated for 2011; emphasize "contributors" in the header as well, which are already mentioned in the body text;

shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)

tuned NEWS

avoid ML structure aliases (especially single-letter abbreviations)

made SML/NJ happy

rename constant u_defl to u_liftdefl; add new constant u_defl :: udom defl -> udom defl

rename constant pdefl to liftdefl_of

Diagnostic command to show locale dependencies.

Documentation for 'interpret' and 'sublocale' with mixins.

Abelian group facts obtained from group facts via interpretation (sublocale).

differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface

remove various lemmas redundant with lub_eq_bottom_iff

change some lemma names containing 'UU' to 'bottom'

renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax; removed redundant lemma UU_least

merged

updated SMT certificates

re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs

tuned whitespace

do not open structure Codegen;

do not open auxiliary ML structures;

uniform treatment of type vs. term environment (cf. b654fa27fbc4); tuned;

uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);

tuned isatest settings;

merged

more robust decomposition of simultaneous goals

function (default) is legacy feature

more scalable Symbol_Pos.explode;

tuned ML toplevel pp for type string: observe depth limit;

theory loader: implicit load path is considered legacy;

explicit file specifications -- avoid secondary load path;

check_file: secondary load path is legacy feature;

share_common_data dummy;

made SML/NJ happy;

made SML/NJ happy;

tuned comments;

made SML/NJ happy; more accurate dependencies;

made SML/NJ happy;

function (tailrec) is a legacy feature

dropped duplicate unused lemmas; spelling

partial_function (tailrec) replaces function (tailrec); dropped unnecessary domain reasoning; curried polydivide_aux

remove lemma ideal_completion.principal_induct2, use principal_induct twice instead

NEWS updates for HOLCF

replaced separate lemmas seq{1,2,3} with seq_simps

changed syntax of powerdomain binary union operators

tuned order of NEWS

NEWS

documentation stub on type_lifting

tuned comments and line breaks

rename function ideal_completion.basis_fun to ideal_completion.extension

fix another proof script broken by a35af5180c01

fix proof script broken by a35af5180c01

merged

full localization with possibly multiple entries; explicit prohibition of fixed type variables

tool-compliant mapper declaration

more proof contexts; formal declaration

mapper is arbitrary term, not only constant; proper backward proofs of derived properties

tuned comment

merged

made SML/NJ happy

check JVM later, to avoid potential conflict with jEdit splash screen;

explicit JVM check on startup;

more explicit jvm_name;

isabelle java: prefer -server here;

configuration option "rule_trace"; discontinued preference "trace-rules";

configuration option "syntax_branching_level";

configuration option "syntax_ast_trace" and "syntax_ast_stat";

more robust ML antiquotations -- allow original tokens without adjacent whitespace;

configuration option "ML_trace";

merged

id_const replaces mk_id

tuned type_lifting declarations

prove more algebraic version of functorial properties; retain old properties for convenience

declare more simp rules, rewrite proofs in Isar-style

merged

use DERIV_intros

generalized monoseq, decseq and incseq; simplified proof for seq_monosub

merged

proper static closures

tuned names

renamed mk_id to the more canonical id_const

merged

better parsing of options, in case the value has '='

show the relation

merged

renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy"

added "sledgehammer_tac" as possible reconstructor in Mirabelle

merged

merged

also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)

Enabled non fully polymorphic map functions in subtyping

make SML/NJ and Poly/ML agree on the type of "before";

only depend on exisiting statements

merged

evaluator separating static and dynamic operations

tuned naming

evaluator separating static and dynamic operations

canonical handling of theory context argument

merged

evaluator separating static and dynamic operations

program is separate argument to serializer

more explicit structure for serializer invocation

merged

tuned proof

HOLogic.mk_id

avoid weird symbols in path

mechanism to keep SMT input and output files around in Mirabelle

proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction

added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)

enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day

Cygwin: Poly/ML 5.4.0 requires libgmp3;

updated to polyml-5.4.0;