structure Graph = Graph;

GraphFun (generic directed graphs); Graph (graphs indexed by strings);

added General/graph.ML: generic direct graphs;

removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line

Removed superfluous arith rules from metric_simps

More Arith.

Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.

nat_arith_tac -> arith_tac

More arith refinements.

tuned README;

Pure/General/symbol.ML;

tuned;

deleted the appendices because documentation exists in the HOL and ZF manuals

defined dquotesoff

new manual ZF

the separate FOL and ZF logics manual, with new material on datatypes and inductive definitions

removal of FOL and ZF

minor updates on inductive definitions and datatypes

fixed titles;

tidying of datatype and inductive definitions

files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;

Refined arithmetic.

congruence rules finally use == instead of = and <->

generalized qed_spec_mp code to work for ZF

datatype package improvements

better qed_spec_mp

Simplified interface.

Simplified arithmetic.

'same' method, 'immediate' proof;

tuned msg;

SYNC;

fixed again;

improved asm_finish;

get_tthms witness theorems;

Split argument structure.

Restructured Arithmatic

*** empty log message ***

verbatim

SYNC;

fixed deriv;

eliminated tthm type and Attribute structure;

tuned msg;

tuned signature;

eliminated global/local names;

eliminated tthm type and Attribute structure;

eliminated tthm type and Attribute structure;

eliminated Attribute structure;

signature BASIC_THM; theorem / axiom deriv: added tags; get/put_name_tags; type attribute;