2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-16 wenzelm 2012-10-16 updated Toplevel.proofs;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-10-16 wenzelm 2012-10-16 more friendly handling of Pure.thy bootstrap errors;
2012-10-16 wenzelm 2012-10-16 more informative error for stand-alone 'qed';
2012-10-16 wenzelm 2012-10-16 further attempts to unify/simplify goal output;
2012-10-16 wenzelm 2012-10-16 more informative error messages of initial/terminal proof methods; more systematic support for sequences with embedded errors; tuned Seq.maps;
2012-10-15 wenzelm 2012-10-15 merged
2012-10-15 bulwahn 2012-10-15 setcomprehension_pointfree simproc also works for set comprehension without an equation
2012-10-15 wenzelm 2012-10-15 tuned message -- avoid extra blank lines;
2012-10-15 wenzelm 2012-10-15 updated to polyml-5.5.0 which reduces chance of HOL-IMP failure (although it is hard to reproduce anyway);
2012-10-14 Markus Kaiser 2012-10-14 store colors after build
2012-10-14 bulwahn 2012-10-14 adding further test cases for the set_comprehension_pointfree simproc
2012-10-14 bulwahn 2012-10-14 refined tactic in set_comprehension_pointfree simproc
2012-10-14 bulwahn 2012-10-14 adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
2012-10-14 bulwahn 2012-10-14 adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
2012-10-14 bulwahn 2012-10-14 extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
2012-10-13 wenzelm 2012-10-13 more informative error of initial/terminal proof steps;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-10-13 wenzelm 2012-10-13 refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;
2012-10-13 wenzelm 2012-10-13 tuned signature;
2012-10-13 wenzelm 2012-10-13 improved adhoc height for small fonts;
2012-10-12 wenzelm 2012-10-12 further refinement of jEdit line range, avoiding lack of final \n;
2012-10-12 wenzelm 2012-10-12 more uniform tooltip color;
2012-10-12 wenzelm 2012-10-12 more NEWS;
2012-10-12 wenzelm 2012-10-12 merged
2012-10-12 traytel 2012-10-12 disambiguated grammar
2012-10-12 traytel 2012-10-12 tuned proofs
2012-10-12 nipkow 2012-10-12 tuned
2012-10-12 wenzelm 2012-10-12 simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with alternative name;
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-12 wenzelm 2012-10-12 discontinued typedef with implicit set_def;
2012-10-12 wenzelm 2012-10-12 merged
2012-10-12 bulwahn 2012-10-12 increading indexes to avoid clashes in the set_comprehension_pointfree simproc
2012-10-12 wenzelm 2012-10-12 no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
2012-10-12 wenzelm 2012-10-12 do not treat interrupt as error here, to avoid confusion in log etc.;
2012-10-12 wenzelm 2012-10-12 more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
2012-10-11 wenzelm 2012-10-11 refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-10-11 wenzelm 2012-10-11 merged
2012-10-11 hoelzl 2012-10-11 cleanup borel_measurable_positive_integral_(fst|snd)
2012-10-11 haftmann 2012-10-11 msetprod based directly on Multiset.fold; pretty syntax for msetprod_image
2012-10-11 haftmann 2012-10-11 avoid global interpretation
2012-10-11 haftmann 2012-10-11 simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets
2012-10-11 wenzelm 2012-10-11 clarified output token markup (see also bc22daeed49e);
2012-10-11 wenzelm 2012-10-11 refined aprop_tr' -- retain entity information by using type slot as adhoc marker;
2012-10-11 wenzelm 2012-10-11 refrain from quantifying outer fixes, to enable nesting of contexts like "context fixes x context assumes A x"; tuned;
2012-10-11 wenzelm 2012-10-11 tuned;
2012-10-11 wenzelm 2012-10-11 tuned;
2012-10-11 wenzelm 2012-10-11 more position information for hyperlink and placement of message;
2012-10-11 wenzelm 2012-10-11 tuned;
2012-10-11 krauss 2012-10-11 mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
2012-10-10 krauss 2012-10-10 removed unused legacy material from mira.py
2012-10-10 wenzelm 2012-10-10 eliminated some remaining uses of typedef with implicit set definition;
2012-10-10 Andreas Lochbihler 2012-10-10 merged
2012-10-10 Andreas Lochbihler 2012-10-10 fix code equation for RBT_Impl.fold
2012-10-10 Andreas Lochbihler 2012-10-10 merged
2012-10-10 Andreas Lochbihler 2012-10-10 tail-recursive implementation for length
2012-10-10 Andreas Lochbihler 2012-10-10 correct definition for skip_black
2012-10-10 wenzelm 2012-10-10 merged