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;

removed norm_typ; improved output; refer to Pretty.pp;

moved read_int etc. to library.ML; added type 'arity';

improved output; refer to Pretty.pp;

Output.add_mode; Output.timing;

output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;

Output.timing;

improved output;

moved print_mode to General/output.ML; load General/pretty.ML early;

added Pure/General/output.ML;

avoid 'handle _' -- would cover Interrupt as well!!!

Sign.infer_types: Sign.pp;

Library.read_int;

Output.output;

'classrel': support multiple arguments;

* ML: all output via channels of writeln etc. passed through Output.output;

output channels;

added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs

new skolemize_tac and skolemize method

new theorem Collect_imp_eq

abstraction over functions is no default any more.

adjusted for different signature of Type.typ_instance

mainly new/different datatype examples

documentation updated

major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)

new default parameters for refute

solver "auto" now issues a warning when it uses solver "enumerate"

Corrected printer bug for bounded quantifiers Q x<=y. P

more group isomorphisms

added drop_take:thm

- deleted unneeded function eta_long (now in Pure/pattern.ML - added HOL.min / HOL.max to allowed consts again - added final simplification step with presburger_ss to preprocessor again

Adapted to new syntax for case expressions.

Added more flexible parse / print translations for case expressions.

Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.

- exported result datatype - added functions get_result and get_exn

updated;

Pure: clear separation of logical types and nonterminals;

adapted tsig/sg interface;

added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;

added fold, product; removed transitive_closure;

adapted names of some sort ops;

major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;

Type.strip_sorts;

incorporate type inference interface from type.ML;

adapted tsig interface;

moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);

test_classrel/arity improve error reporting; tuned;

xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;

string_of_vname moved to term.ML;

incorporate sort ops from term.ML; use Graph.T; misc cleanup;

type.ML now before Syntax module;

xxx_typ_raw replace xxx_typ_no_norm forms;

'classrel' now allows multiple arguments;

Sign.certify_tyname;

TypeInfer.paramify_dummies, TypeInfer.param;

Args.local_typ_raw;

output_tym: removed duplicate clauses;

Graph.minimals;