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;