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;

updated/tuned identifier syntax;

updated notes on sub-/superscripts;

removed Syntax.test_read;

added a lemma lfp_ordinal_induct

fixed the groupI ambiguity

fixed the skolemize method

moved some cardinality results into main HOL

add_dummies no longer uses transform_error but handles specific exception Datatype_Empty instead.

Added exception Datatype_Empty.

mk_id is now also applied to identifiers in test_term.

Groups, Rings and supporting lemmas in ZF

Groups, Rings and supporting lemmas

Groups, Rings and supporting lemmas

avoid Args.list (lost update?);

added has_mode; handle_error: output raw;

Symbol.output;

no token translation / setup for Latex;

HOL: symbolic syntax of Eps;

More readable code.

pretty_thm/goals_aux, pretty_flexpair: pp;

avoid implicit arguments via refs;

Symbol.decode;

added datatype sym, val decode: symbol -> sym;

improved symbolic syntax of Eps: \<some> for mode "epsilon";

removed mlworks and smlnj-0.93 (obsolete);

tuned comments;

moved exception handling back to library.ML;

tuned exeption handling (capture/release);

removed Pure/ML-Systems/mlworks.ML Pure/ML-Systems/polyml-3.x.ML Pure/ML-Systems/smlnj-0.93.ML; added ML-Systems/polyml-time-limit.ML;

obsolete;

Tuned parse_att.

new rules for simplifying quantifiers with Sigma

Add alternative syntax for attributes

Add panic function which exits Isabelle immediately.

Removed ~10000 hack in function idx that can lead to inconsistencies when unifying terms with a large number of abstractions.

Adapted to new name mangling function in code generator.

Adapted to new name mangling function.

Improved name mangling function.

proper use of 'nonterminals';

proper treatment of logical types within syntax;

removed obsolete sort 'logic' and '=?=' syntax;

removed obsolete sort 'logic';

more on bij_betw

tidied

TimeLimit structure added (no proper implementation yet)

including polyml-time-limit.ML

SML/NJs TimeLimit structure ported to Poly/ML

oops -- no Output.out here;

updated;

\<^bsub>/\<^esub> syntax: unbreakable block;

\<^bsub>/\<^esub> syntax: unbreakable block;

Scan.this; tuned;

do *not* export list/list1 -- commas considered special in arg syntax;

target 'generate';

avoid Args.list;

handle raw symbols; Output.add_mode;

handle raw symbols; Output.add_mode; more robust handling of sub/superscript;

tuned _dummy_ofsort syntax;

added pp_show_brackets; support unbreakable blocks;

transform_error;

Library.read_int; Output.output;

improved support for raw symbols;

Output.error;

pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;

added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;