2012-08-30 blanchet 2012-08-30 generate "disc_exhaust" property
2012-08-30 blanchet 2012-08-30 generate "disc_distinct" theorems
2012-08-30 blanchet 2012-08-30 added discriminator theorems
2012-08-30 blanchet 2012-08-30 adjust example
2012-08-30 blanchet 2012-08-30 more work on sugar
2012-08-30 blanchet 2012-08-30 updated Java-related error message
2012-08-30 blanchet 2012-08-30 changed order of arguments to "bnf_sugar"
2012-08-30 blanchet 2012-08-30 define selectors and discriminators
2012-08-30 blanchet 2012-08-30 tuning
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-30 blanchet 2012-08-30 more work on BNF sugar
2012-08-30 blanchet 2012-08-30 renamed ML function for consistency
2012-08-30 blanchet 2012-08-30 started work on datatype sugar
2012-08-30 blanchet 2012-08-30 killed obsolete "bnf_of_typ" command
2012-08-30 blanchet 2012-08-30 removed dead code
2012-08-30 blanchet 2012-08-30 have "bnf_of_typ" command seal the BNF
2012-08-30 wenzelm 2012-08-30 register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-08-30 wenzelm 2012-08-30 refined status of forked goals;
2012-08-30 wenzelm 2012-08-30 proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
2012-08-29 wenzelm 2012-08-29 tuned message;
2012-08-29 wenzelm 2012-08-29 discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;
2012-08-29 wenzelm 2012-08-29 approximative build of pdf documents in 1 pass instead of 3;
2012-08-29 wenzelm 2012-08-29 more formal isabelle makedist from repository;
2012-08-29 wenzelm 2012-08-29 removed remains of generated material, which tends to rot;
2012-08-29 wenzelm 2012-08-29 one more round to ensure that base images are already there, without producing document output themselves;
2012-08-29 wenzelm 2012-08-29 more robust document setup;
2012-08-29 wenzelm 2012-08-29 provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;
2012-08-29 wenzelm 2012-08-29 clarified handling of raw output messages;
2012-08-29 wenzelm 2012-08-29 no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;
2012-08-29 wenzelm 2012-08-29 command 'use' is legacy;
2012-08-29 wenzelm 2012-08-29 clarified separated_chunks vs. space_explode;
2012-08-29 wenzelm 2012-08-29 more precise indentation;
2012-08-29 wenzelm 2012-08-29 modernized specifications;
2012-08-29 wenzelm 2012-08-29 tuned signature;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-29 wenzelm 2012-08-29 init components from local clone that is used to produce the test distribition, which itself lacks Admin;
2012-08-28 wenzelm 2012-08-28 discontinued centralistic changelog;
2012-08-28 wenzelm 2012-08-28 discontinued odd copy of eps logos (cf. 8fc3828fdc8a);
2012-08-28 wenzelm 2012-08-28 prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;
2012-08-28 wenzelm 2012-08-28 removed odd left-over file;
2012-08-28 wenzelm 2012-08-28 update on "isabelle build" and "isabelle build_doc";
2012-08-28 wenzelm 2012-08-28 renamed doc-src to src/Doc; renamed TutorialI to Tutorial;
2012-08-28 wenzelm 2012-08-28 do not hardwire document output options -- to be provided by the user;
2012-08-28 wenzelm 2012-08-28 more permanent update of keywords (cf. 3517d6f50b12);
2012-08-28 wenzelm 2012-08-28 merged
2012-08-28 blanchet 2012-08-28 updated keywords
2012-08-28 blanchet 2012-08-28 fixed import paths in examples
2012-08-28 blanchet 2012-08-28 fixed import paths
2012-08-28 blanchet 2012-08-28 tuning
2012-08-28 blanchet 2012-08-28 updated NEWS and CONTRIBUTORS
2012-08-28 blanchet 2012-08-28 documentation cleanup
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
2012-08-28 webertj 2012-08-28 Typo fixed.
2012-08-28 wenzelm 2012-08-28 updated .hgignore to reflect to (almost) clean result of build_doc;
2012-08-28 wenzelm 2012-08-28 more formal build_doc tool (Admin only); removed some doc-src junk;
2012-08-28 wenzelm 2012-08-28 prepare document more uniformly; fewer latex runs, in accordance to "isabelle document"; apply fixbookmarks last to operate on final root.out;
2012-08-28 wenzelm 2012-08-28 prefer \input which actually checks file existence;