use proper syntactic types for 'syntax' commands

make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion

use full path for library imports

types -> type_synonym

updated NEOS_SERVER, which is now provided via settings;

renamed Sum_Of_Squares to Sum_of_Squares;

Ord_List.merge convenience;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

modernized structure Prop_Logic; avoid ML structure aliases;

added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);

tuned;

tuned;

tuned headers;

merged

adding example theory for list comprehension to set comprehension simproc

adopting proofs due to new list comprehension to set comprehension simproc

adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs

tuned text

merged

removing obselete Id comments from HOL/ex theories

added hints about licensing restrictions and how to enable Z3

tuned

eliminated hard tabs;

allow spaces in $SPASS_HOME value;

tuned;

eliminated alias;

do not open ML structures;

more standard package setup;

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