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;

adapted syntax to cope with lack of non-logical types;

Type.typ_instance;

load ML files only once;

removed duplicate thms;

Sign.typ_instance;

tuned message;

tuned document;

use plain SOME;

proper use of 'syntax';

auto update

has_consts now handles the @-operator

new bij_betw operator

more results about isomorphisms

conversion of Hilbert_Choice to Isar script

the function list1 has been exported.

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.

modified abel_cancel.ML for polymorphic types

simplification for abelian groups

Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy

Comments fixed

lemma disjoint_int_union removed - too special

Change of theory hierarchy: Group is now based in Lattice.

tidied

new atomize theorem

removed a premise of card_inj_on_le

removal of locale coset

deleted redundant proof lines