tuned;

removed unused help function;

new fib example

removal of x-symbol syntax <Sigma> for dependent products

ISABELLE_TMP

path instead of string;

added path;

tuned lexical syntax;

num tokens;

fixed bad link

slight speed improvement

strengthened some theorems

Jerusat settings added

entries for ZChaff and BerkMin added/modified

Oracle corrected

Further development of matrix theory

faster defcnf conversion

updated;

updated;

tuned;

tuned Present.drafts;

added display_drafts and print_drafts commands;

added PRINT_COMMAND setting

added isatool display and isatool print;

print document

display document (in DVI format)

root for draft documents;

Library.translate_string;

added trace (inefficient for very long input);

added translate_string;

added read (provides transition names and sources);

added output_known_symbols; tuned;

added name_of, source_of, source;

added Present.drafts;

added option 'isatool latex -o syms';

An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.

tuned;

improved RemoteFile;

tuned;

Removed this: not really ready yet.

Interface configuration for Isar

Sign.is_logtype;

prs: Output.output;

added split_ext; removed drop_ext;

tuned comment;

Scan.this_string;

tuned representation; added RemoteFile;

tuned;

added this_string;

tuned messages;

added is_logtype (replaces logtypes field of syntax); tuned merge;

removed separate logtypes field of syntax; removed test_read, simple_str_of_sort, simple_string_of_typ; provide default_mode;

removed separate logtypes field of syntax;

Path.split_ext; more robust inform_file_processed;

Sign.is_logtype;

Syntax.default_mode;

added option 'locale=NAME';

Url.File;

* Document preparation: antiquotations provide option 'locale=NAME';

tuned comment;