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

new lemmas

clauses for ordinary resolution

conversion of theorems to atomic form

New simp rules added: insert_disjoint disjoint_insert disjoint_int_union

simpilified and strengthened proofs

fixed latex problems

renamed `> to o_m

changes made due to new Ring_and_Field theory

Eta-expanded function scan_comment to make SmlNJ happy.

broken no longer includes TTP, and other minor changes

removal of prime characters

package needed for superscripts

conversion to clauses for ordinary resolution rather than ME

auto update

Pure: nested comments in inner syntax;

support nested comments;

changed Symbol.beginning;

tuned;

Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);

added Scan.list;

ProofGeneral.process_pgip command;

preparation for integration with new Ring_and_Field.thy

moved first lemma in LongDiv.ML to LongDiv.thy

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

removed Aux.thy;

cleanup up read functions, include liberal versions;

be liberal about constant names;

tuned;

tuned notation;

tuned document;

*** empty log message ***

Add FIXME note re FAIL (is it fixed yet?)

Add cdata output. Add tabs in whitespace. Write two strings instead of Library.quote.

Add -X option to trigger PGIP interaction mode.

*** empty log message ***

replaced Aux.thy by RealLemmas.thy

tuned HOL/record package; enabled record_upd_simproc by default.

improved block sup/sub;

show_structs option;

tuned document;

tidied

auto update

redundant clause removed

solved sml-nj compatibility problem

tuned;

reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.

tuned;

improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers

improved indexed syntax / implicit structures;

tuned;

improved Term.invent_names;

removed 'constdefs' hack;

improved syntax;

improved subscript syntax;

tuned instance statements;

_index1: accomodate improved indexed syntax;

breaks flag;

warning: non-identifier declaration;

added is_keyword;

added is_literal;

more robust output of definitions;