2013-11-25 wenzelm 2013-11-25 NEWS;
2013-11-25 wenzelm 2013-11-25 more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;
2013-11-25 wenzelm 2013-11-25 more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report; more defensive order of Markup.failed vs. Markup.finished, to allow breakdown of ML execution context (see also d7a1973b063c);
2013-11-25 wenzelm 2013-11-25 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
2013-11-24 wenzelm 2013-11-24 Added tag Isabelle2013-2-RC1 for changeset 57aefb80b639
2013-11-23 wenzelm 2013-11-23 more on GTK;
2013-11-22 wenzelm 2013-11-22 reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798 (clone of f6ffe53387ef);
2013-11-21 wenzelm 2013-11-21 NEWS;
2013-11-21 wenzelm 2013-11-21 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command; resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);
2013-11-20 wenzelm 2013-11-20 updated to Isabelle2013-2;
2013-11-20 wenzelm 2013-11-20 compile on Windows (clone of d04576557400);
2013-11-20 wenzelm 2013-11-20 register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37); tuned signature;
2013-12-05 paulson 2013-12-05 updated mirror script for Cambridge
2013-12-05 blanchet 2013-12-05 proper code generation for discriminators/selectors
2013-12-05 blanchet 2013-12-05 reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them
2013-12-05 blanchet 2013-12-05 experiment
2013-12-05 blanchet 2013-12-05 make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
2013-12-05 Andreas Lochbihler 2013-12-05 news
2013-12-05 Andreas Lochbihler 2013-12-05 restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-12-03 panny 2013-12-03 merge
2013-12-02 panny 2013-12-02 generate "code" theorems for incomplete definitions
2013-12-02 blanchet 2013-12-02 updated keywords
2013-12-02 blanchet 2013-12-02 added 'no_code' option
2013-12-02 blanchet 2013-12-02 killed obsolete artifact
2013-12-02 blanchet 2013-12-02 revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
2013-12-02 blanchet 2013-12-02 avoid user-level 'Specification.definition' for low-level definitions
2013-12-02 blanchet 2013-12-02 repaired inconsistency introduced in transiting to 'Local_Theory.define'
2013-12-02 blanchet 2013-12-02 docs for forgotten BNF theorems
2013-12-02 blanchet 2013-12-02 tuning
2013-12-02 blanchet 2013-12-02 added 'cong' attribute to 'map_cong'
2013-12-02 blanchet 2013-12-02 avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)
2013-12-02 blanchet 2013-12-02 don't try to register code equations in a locale with assumptions
2013-12-02 blanchet 2013-12-02 minor doc update
2013-12-02 blanchet 2013-12-02 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
2013-12-02 blanchet 2013-12-02 simpler code
2013-12-01 panny 2013-12-01 more work towards "exhaustive"
2013-11-29 traytel 2013-11-29 Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-28 nipkow 2013-11-28 tuned
2013-11-28 blanchet 2013-11-28 updated docs
2013-11-28 blanchet 2013-11-28 added Riss3g
2013-11-28 blanchet 2013-11-28 reduce dependency (toward move to 'HOL')
2013-11-28 blanchet 2013-11-28 cleaned up indirect dependency
2013-11-28 nipkow 2013-11-28 tuned
2013-11-28 haftmann 2013-11-28 prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
2013-11-28 haftmann 2013-11-28 prefer name-normalizing devarify over unvarifyT whenever appropriate
2013-11-27 traytel 2013-11-27 some documentation
2013-11-27 traytel 2013-11-27 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
2013-11-27 Andreas Lochbihler 2013-11-27 remove junk
2013-11-27 Andreas Lochbihler 2013-11-27 revert 4af7c82463d3 and document type class problem in Haskell
2013-11-27 Andreas Lochbihler 2013-11-27 merged
2013-11-20 Andreas Lochbihler 2013-11-20 no ord instance for String.literal in Haskell when list is also ordered lexicographically
2013-11-20 Andreas Lochbihler 2013-11-20 implement comparisons on String.literal by target-language comparisons
2013-11-20 Andreas Lochbihler 2013-11-20 instantiate linorder for String.literal by lexicographic order
2013-11-20 Andreas Lochbihler 2013-11-20 setup lifting/transfer for String.literal
2013-11-20 Andreas Lochbihler 2013-11-20 add predicate version of lexicographic order on lists
2013-11-26 panny 2013-11-26 merge
2013-11-25 panny 2013-11-25 prevent exception when equations for a function are missing; pave the way for "exhaustive"
2013-11-26 hoelzl 2013-11-26 Add Zorn to HOL-Library
2013-11-26 traytel 2013-11-26 made SML/NJ happier