added discriminator theorems

adjust example

more work on sugar

updated Java-related error message

changed order of arguments to "bnf_sugar"

define selectors and discriminators

tuning

more work on BNF sugar -- up to derivation of nchotomy

more work on BNF sugar

renamed ML function for consistency

started work on datatype sugar

killed obsolete "bnf_of_typ" command

removed dead code

have "bnf_of_typ" command seal the BNF

register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;

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;

some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;

tuned signature;

refined status of forked goals;

proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

tuned message;

discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;

approximative build of pdf documents in 1 pass instead of 3;

more formal isabelle makedist from repository;

removed remains of generated material, which tends to rot;

one more round to ensure that base images are already there, without producing document output themselves;

more robust document setup;

provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;

clarified handling of raw output messages;

no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;

command 'use' is legacy;

clarified separated_chunks vs. space_explode;

more precise indentation;

modernized specifications;

tuned signature;

renamed Position.str_of to Position.here;

init components from local clone that is used to produce the test distribition, which itself lacks Admin;

discontinued centralistic changelog;

discontinued odd copy of eps logos (cf. 8fc3828fdc8a);

prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;

removed odd left-over file;

update on "isabelle build" and "isabelle build_doc";

renamed doc-src to src/Doc; renamed TutorialI to Tutorial;

do not hardwire document output options -- to be provided by the user;

more permanent update of keywords (cf. 3517d6f50b12);

merged

updated keywords

fixed import paths in examples

fixed import paths

tuning

updated NEWS and CONTRIBUTORS

documentation cleanup

added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)

Typo fixed.

updated .hgignore to reflect to (almost) clean result of build_doc;

more formal build_doc tool (Admin only); removed some doc-src junk;

prepare document more uniformly; fewer latex runs, in accordance to "isabelle document"; apply fixbookmarks last to operate on final root.out;

prefer \input which actually checks file existence;

tuned;

prefer (old) isa-index as provided here, to get exactly the same index layout as in Isabelle2012; more accurate ROOT/files;

removed old stuff;

more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;

removed old stuff;

removed historic manual;

more standard document preparation within session context;

more standard document preparation within session context;

updated IsarRef/document/style.sty;

missing file;

removed junk;

more standard document preparation within session context;

removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;

prefer doc-src/pdfsetup.sty; moved IsarRef/Thy/ZF_Specific.thy to ZF/ZF_Isar.thy to avoid dependence of IsarRef on another object-logic;

more official way to set margin;

avoid clash with generated Adaptation.tex on case-insensible file-systems;

missing file;

deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more standard document preparation within session context;

more portable perl invocation;

more standard document preparation within session context;

more standard document preparation within session context; more uniform document build;

more standard document preparation within session context;

clarified "isabelle logo";

clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;

less ambitious test -- terminate more quickly;

tuned;

actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;

test with many add-ons;

updated Theory.begin_theory;

entity markup for theory Pure, to enable hyperlinks etc.;

more accurate defining position of theory;

theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;

fixed theory dependency

more convenient switching of buffers;

report source path and let front-end resolve implicit master location (e.g. URL);

prefer jEdit file name representation (potentially via VFS); tuned;

more precise counting of line/column;

support for direct hyperlinks, without the Hyperlinks plugin;

tuned signature;

some markup for inlined files;

check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;

clarified syntax boundary cases and errors;

simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;

eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

improved errors of parser combinators;

tuned messages: end-of-input rarely means physical end-of-file from the past;

merged

remove Hoare dependency from Fold.thy

added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;