revert changes of already published NEWS;

some updates for release;

more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;

updated Scala/JVM versions;

include trailing comments in proper_command range;

minimal support for x86-mingw;

recognize MacOS on modern Java implementations, notably OpenJDK 1.7;

updated to Scala 2.9.2;

updated headers;

eliminated hard tabs;

Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

NEWS

adapt to changes in RBT_Impl

move RBT implementation into type class contexts

misc tuning; atbroy100 no longer available (?);

NEWS

merged

distributivity of * over Un and UNION

Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *

removed "setsum_set", now subsumed by generic setsum

backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)

tuned README;

direct scala toplevel tools to ISABELLE_JDK_HOME;

simplified component structure;

merged

merged

generalise case certificates to allow ignored parameters

merged

manual merge

dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

more standard method setup;

more precise declaration of goal_tfrees in forked proof state;

partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;

multiset operations are defined with lift_definitions; tuned proofs;

remove outdated comment

rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;

standardized ML aliases;

clarified proof_result: finish proof formally via head tr, not end_tr;

tuned;

more robust Future.fulfill wrt. duplicate assignment and interrupt;

tuned message;

always signal after cancel_group: passive tasks may have become active;

just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;

merged

moved lift_raw_const wrapper out of the Quotient-package into Nominal2

misc tuning and simplification;

static relevance of proof via syntax keywords;

tuned future priorities: print 0, goal ~1, execute ~2;

updated for Poly/ML SVN 1476;

some coverage of HOL/TPTP;

added graph-conversion utility for TPTP files

moved non-interpret-specific code to different module

disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts;

tuned proofs;

slightly faster default compilation of Isabelle/Scala;

more explicit last exec result;

dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;

tuned;

simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;

added ML pretty-printing;

merged

merged

explicit constructor Nat leaves nat_of as conversion

abandoned almost redundant *_foldr lemmas

tuned

no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code

enable parallel proofs (cf. e8552cba702d), only affects packages so far; disable quick_and_dirty to make packages produce proofs -- NB: 'sorry' works via "int" mode of proof commands;

added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);

tuned proofs;

more robust update_perspective, e.g. required after reload of buffer that is not at start position;

tuned imports;

updated header keywords;

init message not bad;

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

discontinued obsolete last_execs (cf. cd3ab7625519);

remove now-unnecessary type annotations from lift_definition commands

more robust generation of quotient rules using tactics

merged

add function dest_Quotient

standardized alias;

fixed document;

merged

correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should

detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr

make Quotient_Def.lift_raw_const working again

use standard quotient lemmas to generate transfer rules

add transfer lemmas for quotients

define reflp directly, in the manner of symp and transp

set up and use lift_definition for word operations

lift_definition declares transfer_rule attribute

configure transfer method for 'a word -> int

added timestamps to logging of named thms

merged

merged

add lemmas for generating transfer rules for typedefs

tuned;

improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;

merge

HOL/Import more precise map types

HOL/Import typed matches against Isabelle typedef result

connect the Quotient package to the Lifting package

support non-open typedefs; define cr_rel in terms of a rep function for typedefs

tuned;

added interpretation for formula conditional;

refactored tptp lex;

refactored tptp yacc to bring close to official spec;

transfer method generalizes over free variables in goal

add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer

update keywords file

merged

fix typos

lift_definition command generates transfer rule

prove_quot_theorem fixes types

documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS

added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; added examples of quickcheck_locale option; trying to speed up Quickcheck_Examples;

stop node execution at first unassigned exec;

discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;

more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned;

less ambitious memo_eval, since memo_result is still not robust here;

less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;

Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;

tuned;

tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

proper signature constraint;

tuned comments;

separate module for prover command execution;